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

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

instance AddGroupCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddGroupCat

theorem AddGroupCat.hasZeroObject.proof_1 : CategoryTheory.Limits.HasZeroObject AddGroupCat

instance GroupCat.instHasZeroObjectGroupCatInstGroupCatLargeCategory : CategoryTheory.Limits.HasZeroObject GroupCat

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

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

instance AddCommGroupCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddCommGroupCat

theorem AddCommGroupCat.hasZeroObject.proof_1 : CategoryTheory.Limits.HasZeroObject AddCommGroupCat

instance CommGroupCat.instHasZeroObjectCommGroupCatInstCommGroupCatLargeCategory : CategoryTheory.Limits.HasZeroObject CommGroupCat