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.

source
def ModuleCat.normalMono {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) (hf : CategoryTheory.Mono f) :
CategoryTheory.NormalMono f

In the category of modules, every monomorphism is normal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ModuleCat.normalEpi {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) (hf : CategoryTheory.Epi f) :
    CategoryTheory.NormalEpi 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
      source
      instance ModuleCat.abelian {R : Type u} [Ring R] :
      CategoryTheory.Abelian (ModuleCat R)

      The category of R-modules is abelian.

      Equations
      • ModuleCat.abelian = CategoryTheory.Abelian.mk
      source
      instance ModuleCat.instHasLimitsOfSizeModuleCatMax {R : Type u} [Ring R] :
      CategoryTheory.Limits.HasLimitsOfSize.{v, v, max v w, max (max (v + 1) (w + 1)) u} (ModuleCatMax R)
      Equations
      • ⋯ = ⋯
      source
      instance ModuleCat.forgetReflectsLimitsOfSize {R : Type u} [Ring R] :
      CategoryTheory.Limits.ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)} (CategoryTheory.forget (ModuleCatMax R))
      Equations
      • ModuleCat.forgetReflectsLimitsOfSize = CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms
      source
      instance ModuleCat.forget₂ReflectsLimitsOfSize {R : Type u} [Ring R] :
      CategoryTheory.Limits.ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)} (CategoryTheory.forget₂ (ModuleCatMax R) AddCommGroupCat)
      Equations
      • ModuleCat.forget₂ReflectsLimitsOfSize = CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms
      source
      instance ModuleCat.forgetReflectsLimits {R : Type u} [Ring R] :
      CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget (ModuleCat R))
      Equations
      • ModuleCat.forgetReflectsLimits = ModuleCat.forgetReflectsLimitsOfSize
      source
      instance ModuleCat.forget₂ReflectsLimits {R : Type u} [Ring R] :
      CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)
      Equations
      • ModuleCat.forget₂ReflectsLimits = ModuleCat.forget₂ReflectsLimitsOfSize
      source
      theorem ModuleCat.exact_iff {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) {O : ModuleCat R} (g : N ⟶ O) :
      CategoryTheory.Exact f g ↔ LinearMap.range f = LinearMap.ker g