hasZeroObject_of_hasTerminal_object

English

If zero morphisms exist, any initial object is a zero object, and similarly any terminal object is a zero object.

Русский

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

LaTeX

$$$[HasZeroMorphisms C]\Rightarrow (HasZeroObject C)\text{ from Initial/Terminal}$$$

Lean4

/-- If there are zero morphisms, any terminal object is a zero object. -/
theorem hasZeroObject_of_hasTerminal_object [HasZeroMorphisms C] [HasTerminal C] : HasZeroObject C :=
  by
  refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩⟩⟩
  calc
    f = 𝟙 _ ≫ f := (Category.id_comp _).symm
    _ = 0 ≫ f := by congr!; subsingleton
    _ = 0 := zero_comp

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