hasZeroObject_of_hasInitial_object

English

If a morphism is both an Iso from initial to zero and compatible with zero morphisms, then it is invertible.

Русский

Если морфизм является изоморфизмом из начального в нулевой объект и совместим с нулевыми морфизмами, он обратим.

LaTeX

$$$IsIso(0:\,X\to X) \land (intrinsic)$$$

Lean4

/-- If there are zero morphisms, any initial object is a zero object. -/
theorem hasZeroObject_of_hasInitial_object [HasZeroMorphisms C] [HasInitial C] : HasZeroObject C :=
  by
  refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩
  calc
    f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _

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