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 Grp.isZero_of_subsingleton (G : Grp) [Subsingleton ↑G] : CategoryTheory.Limits.IsZero G

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

instance Grp.instHasZeroObject : CategoryTheory.Limits.HasZeroObject Grp

instance AddGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddGrp

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

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

instance CommGrp.instHasZeroObject : CategoryTheory.Limits.HasZeroObject CommGrp

instance AddCommGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddCommGrp