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 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 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 = { toPreadditive := ModuleCat.instPreadditive, toIsNormalMonoCategory := ⋯, toIsNormalEpiCategory := ⋯, has_finite_products := ⋯, has_kernels := ⋯, has_cokernels := ⋯ }

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

Add this instance to help Lean with universe levels.

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 (ModuleCat 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₂ (ModuleCat R) AddCommGrp)

instance ModuleCat.forget_reflectsLimits {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) AddCommGrp)