mathlib documentation


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.

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