The category of left R-modules is abelian.

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

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.

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.

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

instance ModuleCat.instHasLimitsOfSizeModuleCatMaxModuleCategory {R : Type u} [Ring R] : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max v w, max (max (v + 1) (w + 1)) u} (ModuleCatMax R)

Equations

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

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

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

instance ModuleCat.forgetReflectsLimits {R : Type u} [Ring R] : CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget (ModuleCat R))

Equations

• ModuleCat.forgetReflectsLimits = ModuleCat.forgetReflectsLimitsOfSize

instance ModuleCat.forget₂ReflectsLimits {R : Type u} [Ring R] : CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)

Equations

• ModuleCat.forget₂ReflectsLimits = ModuleCat.forget₂ReflectsLimitsOfSize

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