# mathlibdocumentation

algebra.category.Module.abelian

# The category of left R-modules is abelian. #

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

noncomputable def Module.normal_mono {R : Type u} [ring R] {M N : Module R} (f : M N) (hf : category_theory.mono f) :

In the category of modules, every monomorphism is normal.

Equations
noncomputable def Module.normal_epi {R : Type u} [ring R] {M N : Module R} (f : M N) (hf : category_theory.epi f) :

In the category of modules, every epimorphism is normal.

Equations
@[protected, instance]
noncomputable def Module.category_theory.abelian {R : Type u} [ring R] :

The category of R-modules is abelian.

Equations
@[protected, instance]
noncomputable def Module.forget_reflects_limits_of_size {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable def Module.forget₂_reflects_limits_of_size {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable def Module.forget_reflects_limits {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable def Module.forget₂_reflects_limits {R : Type u} [ring R] :
Equations
theorem Module.exact_iff {R : Type u} [ring R] {M N : Module R} (f : M N) {O : Module R} (g : N O) :