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

Equations

• AddGroupCat.hasZeroObject = (_ : CategoryTheory.Limits.HasZeroObject AddGroupCat)

instance GroupCat.instHasZeroObjectGroupCatInstGroupCatLargeCategory : CategoryTheory.Limits.HasZeroObject GroupCat

Equations

• 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

Equations

• AddCommGroupCat.hasZeroObject = (_ : CategoryTheory.Limits.HasZeroObject AddCommGroupCat)

instance CommGroupCat.instHasZeroObjectCommGroupCatInstCommGroupCatLargeCategory : CategoryTheory.Limits.HasZeroObject CommGroupCat

Equations

• CommGroupCat.instHasZeroObjectCommGroupCatInstCommGroupCatLargeCategory = (_ : CategoryTheory.Limits.HasZeroObject CommGroupCat)