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.

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.

instance ModuleCat.abelian {R : Type u} [Ring R] : CategoryTheory.Abelian (ModuleCat R)

The category of R-modules is abelian.

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)

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))

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)

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

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

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