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 `has_zero_morphisms` 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 zeroMorphismsOfZeroObject : HasZeroMorphisms C
where
zero X _ := { zero := (default : X ⟶ 0) ≫ default }
zero_comp X {Y Z}
f := by
change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default
rw [Category.assoc]
congr
simp only [eq_iff_true_of_subsingleton]
comp_zero {X Y} f
Z := by
change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default
rw [← Category.assoc]
congr
simp only [eq_iff_true_of_subsingleton]
