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.

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

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

      The category of R-modules is abelian.

      Equations
      • ModuleCat.abelian = CategoryTheory.Abelian.mk
      Equations
      • ModuleCat.forgetReflectsLimitsOfSize = CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms
      Equations
      • ModuleCat.forgetReflectsLimits = ModuleCat.forgetReflectsLimitsOfSize
      Equations
      • ModuleCat.forget₂ReflectsLimits = ModuleCat.forget₂ReflectsLimitsOfSize