mathlib3 documentation

algebra.category.Group.abelian

The category of abelian groups is abelian #

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

source
noncomputable 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
noncomputable 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
@[protected, instance]
noncomputable def AddCommGroup.category_theory.abelian  :
category_theory.abelian AddCommGroup

The category of abelian groups is abelian.

Equations