Documentation

Mathlib.Algebra.Category.Grp.Abelian

The category of abelian groups is abelian #

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

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

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

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

      Equations
        Instances For
          source
          instance AddCommGrp.instAbelian :
          CategoryTheory.Abelian AddCommGrp

          The category of abelian groups is abelian.

          Equations