mathlib documentation

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.

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

The category of R-modules is abelian.

Equations
theorem Module.exact_iff {R : Type u} [ring R] {M N : Module R} (f : M N) {O : Module R} (g : N O) :