The category of (commutative) (additive) groups has a zero object.

AddCommGroup also has zero morphisms. For definitional reasons, we infer this from preadditivity rather than from the existence of a zero object.

theorem GrpCat.isZero_of_subsingleton (G : GrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G

theorem AddGrpCat.isZero_of_subsingleton (G : AddGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G

instance GrpCat.instHasZeroObject : CategoryTheory.Limits.HasZeroObject GrpCat

instance AddGrpCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddGrpCat

theorem GrpCat.subsingleton_of_isZero {G : GrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G

theorem AddGrpCat.subsingleton_of_isZero {G : AddGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G

theorem GrpCat.isZero_iff_subsingleton {G : GrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G

theorem AddGrpCat.isZero_iff_subsingleton {G : AddGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G

theorem CommGrpCat.isZero_of_subsingleton (G : CommGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G

theorem AddCommGrpCat.isZero_of_subsingleton (G : AddCommGrpCat) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G

instance CommGrpCat.instHasZeroObject : CategoryTheory.Limits.HasZeroObject CommGrpCat

instance AddCommGrpCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddCommGrpCat

theorem CommGrpCat.subsingleton_of_isZero {G : CommGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G

theorem AddCommGrpCat.subsingleton_of_isZero {G : AddCommGrpCat} (h : CategoryTheory.Limits.IsZero G) : Subsingleton ↑G

theorem CommGrpCat.isZero_iff_subsingleton {G : CommGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G

theorem AddCommGrpCat.isZero_iff_subsingleton {G : AddCommGrpCat} : CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G