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

Equations

• Grp.instHasZeroObject = ⋯

instance AddGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddGrp

Equations

• AddGrp.hasZeroObject = ⋯

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

Equations

• CommGrp.instHasZeroObject = ⋯

instance AddCommGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddCommGrp

Equations

• AddCommGrp.hasZeroObject = ⋯