English
If j is initial in J, then the injection colimit.ι F j is an isomorphism for any F with a colimit.
Русский
Если j начальный в J, то инъекция colimit.ι F j является изоморфизмом.
LaTeX
$$$$\\text{If } I:\\ IsInitial\\ j\\; \\text{ and } F:\\; J \\to C,\\; [HasColimit F],\\; [\\forall f, IsIso(F.map f)]\\Rightarrow \\mathrm{IsIso}(\\mathrm{colimit}.\\ι F j).$$$$
Lean4
theorem isIso_ι_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasColimit F]
[∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F j) :=
⟨⟨colimit.desc _ (coconeOfDiagramInitial I F), by
refine ⟨?_, by ext; simp⟩
dsimp;
simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app, Functor.const_obj_obj,
IsInitial.to_self, Functor.map_id]
dsimp [inv]; simp only [Category.id_comp, Category.comp_id, and_self]
apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _⟩⟩
