Functorial projective resolutions of modules

The fact that an R-module M can be functorially written as a quotient of a projective R-module is expressed as the definition ModuleCat.projectiveResolution. Using the construction in the file Mathlib/Algebra/Homology/LeftResolution/Basic.lean, we may obtain a functor (projectiveResolution R).chainComplexFunctor which sends M : ModuleCat R to a projective resolution.

instance ModuleCat.instProjectiveObjFree (R : Type u) [Ring R] (X : Type u) : CategoryTheory.Projective ((free R).obj X)

noncomputable def ModuleCat.projectiveResolution (R : Type u) [Ring R] : CategoryTheory.Abelian.LeftResolution (CategoryTheory.isProjective (ModuleCat R)).ι

An R-module M can be functorially written as a quotient of a projective R-module.

Equations

• One or more equations did not get rendered due to their size.