CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts
theorem CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {ι : Type v}
{B : ι → C}, (∀ (A : C), ∃ i, Nonempty (B i ⟶ A)) → ∃ T, ∀ (X : C), Nonempty (T ⟶ X)
The theorem `CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts` states that if a category `C` has (small) products and a small weakly initial set of objects (which is a set of objects such that for any object `A` in `C`, there exists an object in the set that has a morphism to `A`), then `C` has a weakly initial object. In other words, there exists an object `T` in `C` such that for every other object `X` in `C`, there is a morphism from `T` to `X`.
More concisely: If a category has small products and a small set of objects with a morphism to every object, then it has a weakly initial object.
|
CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers
theorem CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasWideEqualizers C]
{T : C}, (∀ (X : C), Nonempty (T ⟶ X)) → CategoryTheory.Limits.HasInitial C
The theorem `CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers` states that if a category `C` has small wide equalizers and a weakly initial object `T` (an object such that there exists at least one morphism from `T` to any object `X` in `C`), then `C` has an initial object. The initial object is specifically constructed as the wide equalizer of all endomorphisms on the weakly initial object `T`.
In simpler terms, if a category has a certain type of structure (small wide equalizers) and an object that has at least one arrow to every other object (a weakly initial object), then it also has an object from which there is exactly one arrow to every other object (an initial object).
More concisely: If a category has small wide equalizers and a weakly initial object, then it has an initial object as the wide equalizer of all endomorphisms on the weakly initial object.
|