The category of abelian groups is abelian

def AddCommGroupCat.normalMono {X : AddCommGroupCat} {Y : AddCommGroupCat} (f : X ⟶ Y) : CategoryTheory.Mono f → CategoryTheory.NormalMono f

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

def AddCommGroupCat.normalEpi {X : AddCommGroupCat} {Y : AddCommGroupCat} (f : X ⟶ Y) : CategoryTheory.Epi f → CategoryTheory.NormalEpi f

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

instance AddCommGroupCat.instAbelianAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Abelian AddCommGroupCat

The category of abelian groups is abelian.

theorem AddCommGroupCat.exact_iff {X : AddCommGroupCat} {Y : AddCommGroupCat} {Z : AddCommGroupCat} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.Exact f g ↔ AddMonoidHom.range f = AddMonoidHom.ker g

instance AddCommGroupCat.instPreservesFiniteLimitsFunctorAddCommGroupCatInstAddCommGroupCatLargeCategoryCategoryColimHasColimitsOfShapeOfHasColimitsOfSizeInstHasColimitsOfSizeAddCommGroupCatMaxInstAddCommGroupCatLargeCategory_3 {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim

The category of abelian groups satisfies Grothedieck's Axiom AB5.