Finite projective dimension under flat base change and faithfully flat descent

Let S be an R-algebra. Extension of scalars along S preserves finite projective dimension when S is flat, and reflects it when S is faithfully flat: for every R-module M,

M is m-fpd over R  ↔  S ⊗[R] M is m-fpd over S.

For a pseudocoherent module, for instance a finite module over a noetherian ring, this says that M and S ⊗[R] M have the same projective dimension. Consequently a noetherian ring has global dimension at most that of any faithfully flat algebra over it; see TauCeti.globalDimension_le_of_faithfullyFlat.

This is the homological half of the descent of regularity along faithfully flat homomorphisms of noetherian local rings: if R → S is such a homomorphism and S is regular, then the residue field of R has finite projective dimension over R, which by Serre's criterion makes R regular.

Main results

• TauCeti.Module.IsFPD.baseChange: flat base change preserves finite projective dimension.
• TauCeti.Module.IsFPD.of_baseChange: faithfully flat base change reflects finite projective dimension.
• TauCeti.Module.isFPD_baseChange_iff: the two combined.
• ModuleCat.hasProjectiveDimensionLE_baseChange_iff: a pseudocoherent module has projective dimension at most n exactly when its faithfully flat base change does.

References

• H. Matsumura, Commutative Ring Theory, Theorem 23.7, for the descent of regularity along flat local homomorphisms, which this descent of projective dimension feeds.

theorem TauCeti.Module.IsFPD.baseChange {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] {M : Type w} [AddCommGroup M] [Module R M] [Module.Flat R S] {m : ℕ} (h : IsFPD R M m) : IsFPD S (TensorProduct R S M) m

Flat base change preserves finite projective dimension. If M is m-fpd over R and S is a flat R-algebra, then S ⊗[R] M is m-fpd over S.

theorem TauCeti.Module.IsFPD.of_baseChange {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] {M : Type w} [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] {m : ℕ} (h : IsFPD S (TensorProduct R S M) m) : IsFPD R M m

Faithfully flat base change reflects finite projective dimension. If S is a faithfully flat R-algebra and S ⊗[R] M is m-fpd over S, then M is m-fpd over R.

theorem TauCeti.Module.isFPD_baseChange_iff {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] {M : Type w} [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] {m : ℕ} : IsFPD S (TensorProduct R S M) m ↔ IsFPD R M m

Faithfully flat base change detects finite projective dimension. An R-module M is m-fpd exactly when S ⊗[R] M is m-fpd over a faithfully flat R-algebra S.

theorem ModuleCat.hasProjectiveDimensionLE_baseChange_iff {R S M : Type u} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] (hM : TauCeti.Huber.IsPseudoCoherentOver R M ⊤) {n : ℕ} : CategoryTheory.HasProjectiveDimensionLE (↧(TensorProduct R S M)) n ↔ CategoryTheory.HasProjectiveDimensionLE (↧M) n

Faithfully flat base change preserves and detects projective dimension. A pseudocoherent R-module M, for instance a finite module over a noetherian ring, has projective dimension at most n exactly when S ⊗[R] M has projective dimension at most n over a faithfully flat R-algebra S.