English
If a certain isUniversalColimit holds, then the category has strict initial objects.
Русский
Если соблюдается некое универсальное свойство колимита, то в категории существуют строгие начальные объекты.
LaTeX
$$$IsUniversalColimit( BinaryCofan.mk( id, id )) \\Rightarrow HasStrictInitialObjects C$$$
Lean4
theorem hasStrictInitial_of_isUniversal [HasInitial C] (H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))) :
HasStrictInitialObjects C :=
hasStrictInitialObjects_of_initial_is_strict
(by
intro A f
suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
by
obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
rcases (Category.id_comp _).symm.trans h₂ with rfl
exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> simp) (mapPair_equifibered _) ?_).some
rintro ⟨⟨⟩⟩ <;> dsimp <;> exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩)
