mathlib documentation

algebra.category.Group.abelian

The category of abelian groups is abelian

source
def AddCommGroup.normal_mono {X Y : AddCommGroup} (f : X ⟶ Y) (hf : category_theory.mono f) :
category_theory.normal_mono f

In the category of abelian groups, every monomorphism is normal.

Equations
source
def AddCommGroup.normal_epi {X Y : AddCommGroup} (f : X ⟶ Y) (hf : category_theory.epi f) :
category_theory.normal_epi f

In the category of abelian groups, every epimorphism is normal.

Equations
source
@[instance]
def AddCommGroup.category_theory.abelian  :
category_theory.abelian AddCommGroup

The category of abelian groups is abelian.

Equations