Lean4
/-- A category with a zero object has zero morphisms.
It is rarely a good idea to use this. Many categories that have a zero object have zero
morphisms for some other reason, for example from additivity. Library code that uses
`zeroMorphismsOfZeroObject` will then be incompatible with these categories because
the `HasZeroMorphisms` instances will not be definitionally equal. For this reason library
code should generally ask for an instance of `HasZeroMorphisms` separately, even if it already
asks for an instance of `HasZeroObjects`. -/
def hasZeroMorphisms {O : C} (hO : IsZero O) : HasZeroMorphisms C
where
zero X Y := { zero := hO.from_ X ≫ hO.to_ Y }
zero_comp X {Y Z}
f := by
change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
rw [Category.assoc]
congr
apply hO.eq_of_src
comp_zero {X Y} f
Z := by
change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
rw [← Category.assoc]
congr
apply hO.eq_of_tgt
