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 = CategoryTheory.Abelian.mk

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯