mathlib documentation

algebra.category.Group.zero

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.

@[protected, instance]

def AddGroup.has_zero_object :

category_theory.limits.has_zero_object AddGroup

Equations

AddGroup.has_zero_object = {zero := 0, unique_to := λ (X : AddGroup), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : AddGroup), {to_inhabited := {default := 0}, uniq := _}}

@[protected, instance]

def Group.category_theory.limits.has_zero_object :

category_theory.limits.has_zero_object Group

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 := _}}

@[protected, instance]

def CommGroup.category_theory.limits.has_zero_object :

category_theory.limits.has_zero_object CommGroup

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 := _}}

@[protected, instance]

def AddCommGroup.has_zero_object :

category_theory.limits.has_zero_object AddCommGroup

Equations

AddCommGroup.has_zero_object = {zero := 0, unique_to := λ (X : AddCommGroup), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : AddCommGroup), {to_inhabited := {default := 0}, uniq := _}}