mathlib3 documentation

algebra.category.Group.zero

The category of (commutative) (additive) groups has a zero object. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

AddCommGroup also has zero morphisms. For definitional reasons, we infer this from preadditivity rather than from the existence of a zero object.

source
theorem Group.is_zero_of_subsingleton (G : Group) [subsingleton ↥G] :
category_theory.limits.is_zero G
source
theorem AddGroup.is_zero_of_subsingleton (G : AddGroup) [subsingleton ↥G] :
category_theory.limits.is_zero G
source
@[protected, instance]
def AddGroup.has_zero_object  :
category_theory.limits.has_zero_object AddGroup
source
@[protected, instance]
def Group.category_theory.limits.has_zero_object  :
category_theory.limits.has_zero_object Group
source
theorem AddCommGroup.is_zero_of_subsingleton (G : AddCommGroup) [subsingleton ↥G] :
category_theory.limits.is_zero G
source
theorem CommGroup.is_zero_of_subsingleton (G : CommGroup) [subsingleton ↥G] :
category_theory.limits.is_zero G
source
@[protected, instance]
def CommGroup.category_theory.limits.has_zero_object  :
category_theory.limits.has_zero_object CommGroup
source
@[protected, instance]
def AddCommGroup.has_zero_object  :
category_theory.limits.has_zero_object AddCommGroup