Finite projective dimension and the Cartan map

Over a left Noetherian ring, a finitely generated module of projective dimension at most n admits a resolution of length at most n by finitely generated projectives. Successive finite free surjections have finitely generated kernels, and dimension shifting makes the last kernel projective.

Consequently, if every finitely generated module has finite projective dimension, the Cartan map is bijective. No uniform bound is required. In particular this applies when the projective dimensions of all modules have a common finite bound.

References

• Charles A. Weibel, The K-book, Chapter II, Section 7, for the resolution theorem.
• Charles A. Weibel, An Introduction to Homological Algebra, Sections 2.2 and 4.1, for finite projective resolutions and dimension shifting.

The induction refines Mathlib's CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.iff_hasProjectiveDimensionLE by choosing finite free covers, retaining finite generation, and constructing explicit TauCeti.ExactStructure.FiniteResolution data. The dimension-shifting step uses CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff.

theorem TauCeti.exists_finiteProjectiveResolution_of_hasProjectiveDimensionLE {R : Type u} [Ring R] [IsNoetherianRing R] {M : ModuleCat R} [Module.Finite R ↑M] {n : ℕ} (hM : CategoryTheory.HasProjectiveDimensionLE M n) : ∃ (r : (ExactStructure.abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) M), r.length ≤ n

A finite projective-dimension bound on a finitely generated module over a left Noetherian ring is realized by a finite resolution of the same length bound, with finitely generated projective terms.

theorem TauCeti.finiteModules_le_admitsFiniteResolution_of_finite_projectiveDimension {R : Type u} [Ring R] [IsNoetherianRing R] (h : ∀ (M : ModuleCat R), Module.Finite R ↑M → ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE M n) : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)

Finite projective dimension of every finitely generated module supplies the finite-resolution hypothesis of the Cartan comparison theorem. The bound may depend on the module.

theorem TauCeti.cartanMap_bijective_of_finite_projectiveDimension {R : Type u} [Ring R] [IsNoetherianRing R] (h : ∀ (M : ModuleCat R), Module.Finite R ↑M → ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE M n) : Function.Bijective ⇑(cartanMap R)

The Cartan map is bijective over a left Noetherian ring when every finitely generated module has finite projective dimension. In particular, finite global dimension suffices.