isIso_of_isInitial — Mathlib

English

Any morphism between initial objects is an isomorphism.

Русский

Любой морфизм между начальными объектами является изоморфизмом.

LaTeX

$$$\\forall X,Y,\\text{IsInitial } X, \\text{IsInitial } Y \\Rightarrow \\text{IsIso }(f:X\\to Y)$$$

Lean4

/-- Any morphism between initial objects is an isomorphism. -/
theorem isIso_of_isInitial {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) : IsIso f :=
  by
  refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
  simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
  apply IsInitial.hom_ext hX

Похожие утверждения