English
If C has wide equalizers and T is a weakly initial object (i.e., maps T → X exist for every X), then C has an initial object. The initial object is constructed as the wide equalizer of all endomorphisms of T.
Русский
Если у C есть широкие эквалайзеры и имеется слабовводимый объект T, то C имеет начальный объект. Начальный объект строится как широкий эквалайзер всех эндоморфизмов T.
LaTeX
$$$$\text{HasInitial } C,$$$$
Lean4
/-- 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.
-/
theorem hasInitial_of_weakly_initial_and_hasWideEqualizers [HasWideEqualizers.{v} C] {T : C}
(hT : ∀ X, Nonempty (T ⟶ X)) : HasInitial C :=
by
let endos := T ⟶ T
let i := wideEqualizer.ι (id : endos → endos)
haveI : Nonempty endos := ⟨𝟙 _⟩
have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) :=
by
intro X
refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
let E := equalizer a (i ≫ Classical.choice (hT _))
let e : E ⟶ wideEqualizer id := equalizer.ι _ _
let h : T ⟶ E := Classical.choice (hT E)
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
rw [Category.assoc, Category.assoc]
apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
rw [Category.comp_id, cancel_mono_id i] at this
haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
rw [← cancel_epi e]
apply equalizer.condition
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))
