Documentation

Mathlib.Algebra.Category.Grp.Abelian

The category of abelian groups is abelian #

source
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.
Instances For
    source
    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.
    Instances For
      source
      instance AddCommGrp.instAbelian :
      CategoryTheory.Abelian AddCommGrp

      The category of abelian groups is abelian.

      Equations