Constructions related to weakly initial objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
category_theory.has_weakly_initial_of_weakly_initial_set_and_has_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{ι : Type v}
{B : ι → C}
(hB : ∀ (A : C), ∃ (i : ι), nonempty (B i ⟶ A)) :
If C has (small) products and a small weakly initial set of objects, then it has a weakly initial
object.
theorem
category_theory.has_initial_of_weakly_initial_and_has_wide_equalizers
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_wide_equalizers C]
{T : C}
(hT : ∀ (X : C), nonempty (T ⟶ X)) :
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.