The category of abelian groups is abelian

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

instance AddCommGrp.instAbelian : CategoryTheory.Abelian AddCommGrp

The category of abelian groups is abelian.

Equations

• AddCommGrp.instAbelian = CategoryTheory.Abelian.mk

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

instance AddCommGrp.instPreservesFiniteLimitsFunctorColimOfIsFiltered {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.

Equations

• AddCommGrp.instPreservesFiniteLimitsFunctorColimOfIsFiltered = CategoryTheory.Limits.colim.preservesFiniteLimitsOfMapExact ⋯