Theorems · Theorem · category theory

CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C] {T : C},
  (∀ (X : C), Nonempty (T ⟶ X)) → CategoryTheory.Limits.HasInitial C

If C has (small) wide equalizers and a weakly initial object, then it has an initial object. The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly initial object.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Cited by

0 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWideEqualizers