Projective dimension under flat and faithfully flat base change

Let S be an R-algebra and M an R-module. If S is flat over R, base change carries a projective resolution of M to a projective resolution of S ⊗[R] M, so

pd_S (S ⊗[R] M) ≤ pd_R M.

If moreover S is faithfully flat, R is Noetherian and M is finite, the two projective dimensions are equal. The point is that projectivity of a finitely presented module descends along a faithfully flat map: projective modules are flat, flatness descends by Mathlib's Module.Flat.of_flat_tensorProduct, and a finitely presented flat module is projective. Over a Noetherian ring the syzygies of a finite module are again finite, so dimension shifting along a finite free presentation 0 → K → P → M → 0, which stays exact after base change, reduces the comparison in every degree to this descent of projectivity.

This is the module-theoretic step in the descent of regularity along flat local homomorphisms (Matsumura, Theorem 23.7 (i)): if R → S is a flat local homomorphism of Noetherian local rings and S is regular, every finite R-module, in particular the residue field of R, has projective dimension at most dim S, and Serre's characterization of regular local rings by finite global dimension then makes R regular.

Main results

• Module.Projective.of_projective_tensorProduct: projectivity of a finitely presented module descends along a faithfully flat algebra.
• ModuleCat.hasProjectiveDimensionLT_tensorProduct: flat base change does not increase projective dimension.
• ModuleCat.hasProjectiveDimensionLT_of_tensorProduct: for a finite module over a Noetherian ring, a bound on the projective dimension descends along a faithfully flat algebra.
• ModuleCat.projectiveDimension_tensorProduct: faithfully flat base change preserves the projective dimension of a finite module over a Noetherian ring.

References

• H. Matsumura, Commutative Ring Theory, Theorem 23.7.
• Stacks Project, Tag 00NX: finitely presented flat modules are projective.

theorem Module.Projective.of_projective_tensorProduct (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (S : Type u_3) [CommRing S] [Algebra R S] [FaithfullyFlat R S] [FinitePresentation R M] [Projective S (TensorProduct R S M)] : Projective R M

Projectivity of a finitely presented module descends along a faithfully flat algebra.

@[simp]

theorem Module.Projective.iff_projective_tensorProduct {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (S : Type u_3) [CommRing S] [Algebra R S] [FaithfullyFlat R S] [FinitePresentation R M] : Projective S (TensorProduct R S M) ↔ Projective R M

A finitely presented module is projective exactly when its base change to a faithfully flat algebra is.

theorem ModuleCat.hasProjectiveDimensionLT_tensorProduct {R : Type u} [CommRing R] [Small.{w, u} R] (S : Type v) [CommRing S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R S] {n : ℕ} (h : CategoryTheory.HasProjectiveDimensionLT (↧M) n) : CategoryTheory.HasProjectiveDimensionLT (↧(TensorProduct R S M)) n

Flat base change does not increase projective dimension. If S is a flat R-algebra and M has projective dimension less than n over R, then S ⊗[R] M has projective dimension less than n over S.

theorem ModuleCat.hasProjectiveDimensionLT_of_tensorProduct {R : Type u} [CommRing R] [Small.{w, u} R] (S : Type v) [CommRing S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] [IsNoetherianRing R] [Module.Finite R M] {n : ℕ} (h : CategoryTheory.HasProjectiveDimensionLT (↧(TensorProduct R S M)) n) : CategoryTheory.HasProjectiveDimensionLT (↧M) n

Faithfully flat descent of projective dimension. Let S be a faithfully flat algebra over a Noetherian ring R and M a finite R-module. If S ⊗[R] M has projective dimension less than n over S, then M has projective dimension less than n over R.

@[simp]

theorem ModuleCat.hasProjectiveDimensionLT_tensorProduct_iff {R : Type u} [CommRing R] [Small.{w, u} R] (S : Type v) [CommRing S] [Algebra R S] {M : Type w} [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] [IsNoetherianRing R] [Module.Finite R M] {n : ℕ} : CategoryTheory.HasProjectiveDimensionLT (↧(TensorProduct R S M)) n ↔ CategoryTheory.HasProjectiveDimensionLT (↧M) n

For a finite module over a Noetherian ring and a faithfully flat algebra S, a bound on the projective dimension holds before base change to S exactly when it holds after.

theorem ModuleCat.projectiveDimension_tensorProduct_le {R : Type u} [CommRing R] [Small.{w, u} R] (S : Type v) [CommRing S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R S] : CategoryTheory.projectiveDimension ↧(TensorProduct R S M) ≤ CategoryTheory.projectiveDimension ↧M

Flat base change does not increase projective dimension: pd_S (S ⊗[R] M) ≤ pd_R M for every R-module M.

@[simp]

theorem ModuleCat.projectiveDimension_tensorProduct {R : Type u} [CommRing R] [Small.{w, u} R] (S : Type v) [CommRing S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R S] [IsNoetherianRing R] [Module.Finite R M] : CategoryTheory.projectiveDimension ↧(TensorProduct R S M) = CategoryTheory.projectiveDimension ↧M

Faithfully flat base change preserves projective dimension of a finite module over a Noetherian ring: pd_S (S ⊗[R] M) = pd_R M.