instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms

English

If there are zero morphisms, then IsZero is closed under subobjects.

Русский

Если существуют нулевые морфизмы, IsZero замкнуто по подобъектам.

LaTeX

$$$\forall C [\mathbf{Category}(C)], [\mathbf{HasZeroMorphisms} C] \Rightarrow \mathrm{IsClosedUnderSubobjects}(\mathrm{IsZero}(C)).$$$

Lean4

instance [HasZeroMorphisms C] : IsClosedUnderSubobjects (IsZero (C := C)) where
  prop_of_mono f _ hX := IsZero.of_mono f hX

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