Functorial projective resolutions of modules

The fact that a 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 Algebra.Homology.LeftResolution.Basic, 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)).ι

A 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.