Finite projective resolutions of modules of finite projective dimension

Over a left Noetherian ring, a finitely generated module M of projective dimension at most n has a projective resolution F → M, in the sense of Mathlib's CategoryTheory.ProjectiveResolution, whose terms are finitely generated projective modules and vanish above degree n. The minimal finite free refinement over a Noetherian local ring is provided in TauCeti.Algebra.Category.ModuleCat.Projective.MinimalResolution.ChainComplex.

This is the form in which a bound on the projective dimension of a module, such as the residue field of a local ring, enters arguments with explicit resolutions: comparison maps into the resolution are chain maps of projective resolutions, and over a local ring the ranks of its terms are defined.

The resolution is the chain complex of the finite resolution of TauCeti.exists_finiteProjectiveResolution_of_hasProjectiveDimensionLE, obtained by iterating finite free surjections and dimension shifting, made into a projective resolution by TauCeti.ExactStructure.FiniteResolution.toProjectiveResolution.

Main results

• ModuleCat.exists_projectiveResolution_finite: over a left Noetherian ring, a finite module of projective dimension at most n has a projective resolution by finite projective modules vanishing above degree n.

References

• Stacks Project, Tag 0CXF.
• Charles A. Weibel, An Introduction to Homological Algebra, Section 4.1, for projective dimension and dimension shifting.

theorem TauCeti.ExactStructure.FiniteResolution.finite_toProjectiveResolution_X {R : Type u} [Ring R] {M : ModuleCat R} (r : (abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) M) (hP : finiteProjectiveModules R ≤ CategoryTheory.isProjective (ModuleCat R)) (i : ℕ) : Module.Finite R ↑((toProjectiveResolution hP r).complex.X i)

Converting a finite resolution by finite projective modules to a projective resolution preserves finiteness of every term, including the zero terms above its length.

theorem ModuleCat.exists_projectiveResolution_finite {R : Type u} [Ring R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] {n : ℕ} (hM : CategoryTheory.HasProjectiveDimensionLE M n) : ∃ (F : CategoryTheory.ProjectiveResolution M), (∀ (i : ℕ), Module.Finite R ↑(F.complex.X i)) ∧ ∀ (i : ℕ), n < i → CategoryTheory.Limits.IsZero (F.complex.X i)

Finite projective resolutions. Over a left Noetherian ring, a finitely generated module of projective dimension at most n has a projective resolution whose terms are finitely generated and vanish above degree n.