Finite-term projective resolutions of finite modules

Over a noetherian commutative ring, a finite module admits a projective resolution whose terms remain finite. Construct the resolution in FGModuleCat, where Mathlib's ProjectiveResolution.of applies after the finite-free epimorphisms give enough projectives. The inclusion into ModuleCat preserves homology; its preservation of projectives follows because a projective finite module is a retract of a finite free module.

The same witness, extended to integer-indexed cochain degrees, is strictly bounded above by zero, termwise finite and projective, with a quasi-isomorphism to the degree-zero complex of the input module. The strict bound, projectivity and quasi-isomorphism are supplied by Mathlib's ProjectiveResolution API; the theorem below supplies finiteness in both indexings. The negative-degree tail is not asserted to terminate. This is a resolution of one module, not a finite-projective model of an arbitrary bounded complex.

theorem ModuleCat.exists_finite_projectiveResolution {R : Type u} [CommRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] : ∃ (P : CategoryTheory.ProjectiveResolution M), (∀ (n : ℕ), Module.Finite R ↑(P.complex.X n)) ∧ ∀ (i : ℤ), Module.Finite R ↑(P.cochainComplex.X i)

A finite module over a noetherian commutative ring has a projective resolution with finite terms in both the natural-number chain indexing and its integer cochain extension. The latter is strictly supported in degrees at most zero.