Documentation

Mathlib.Algebra.Category.GroupCat.Abelian

The category of abelian groups is abelian #

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance AddCommGroupCat.instAbelianAddCommGroupCatInstAddCommGroupCatLargeCategory :
      CategoryTheory.Abelian AddCommGroupCat

      The category of abelian groups is abelian.

      Equations
      source
      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
      source
      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.

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