Constructions related to weakly initial objects

This file gives constructions related to weakly initial objects, namely:

• If a category has small products and a small weakly initial set of objects, then it has a weakly initial object.
• If a category has wide equalizers and a weakly initial object, then it has an initial object.

These are primarily useful to show the General Adjoint Functor Theorem.

theorem CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts {C : Type u} [Category.{v, u} C] [Limits.HasProducts C] {ι : Type w} {B : ι → C} (hB : ∀ (A : C), ∃ (i : ι), Nonempty (B i ⟶ A)) : ∃ (T : C), ∀ (X : C), Nonempty (T ⟶ X)

If C has (small) products and a small weakly initial set of objects, then it has a weakly initial object.

theorem CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers {C : Type u} [Category.{v, u} C] [Limits.HasWideEqualizers C] {T : C} [LocallySmall.{w, v, u} C] (hT : ∀ (X : C), Nonempty (T ⟶ X)) : 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.