Documentation

Mathlib.Algebra.Category.ModuleCat.Abelian

The category of left R-modules is abelian. #

Additionally, two linear maps are exact in the categorical sense iff range f = ker g.

In the category of modules, every monomorphism is normal.

Instances For
    def ModuleCat.normalEpi {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M N) (hf : CategoryTheory.Epi f) :

    In the category of modules, every epimorphism is normal.

    Instances For

      The category of R-modules is abelian.

      theorem ModuleCat.exact_iff {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M N) {O : ModuleCat R} (g : N O) :