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.
@[instance]
Equations
- Group.category_theory.limits.has_zero_object = {zero := 1, unique_to := λ (X : Group), {to_inhabited := {default := 1}, uniq := _}, unique_from := λ (X : Group), {to_inhabited := {default := 1}, uniq := _}}
@[instance]
Equations
- CommGroup.category_theory.limits.has_zero_object = {zero := 1, unique_to := λ (X : CommGroup), {to_inhabited := {default := 1}, uniq := _}, unique_from := λ (X : CommGroup), {to_inhabited := {default := 1}, uniq := _}}