Global dimension of regular rings

Let R be a regular ring of finite Krull dimension d. Every R-module, finitely generated or not, has projective dimension at most d. For a regular local ring the bound is attained by the residue field, so the global dimension of a regular local ring is its Krull dimension.

Conversely (Serre), a Noetherian local ring whose residue field has finite projective dimension is regular. Together with the bound above, a Noetherian local ring has finite global dimension exactly when it is regular. As localization does not increase the global dimension, every localization of a regular local ring at a prime is again a regular local ring, so a regular local ring is a regular ring in Mathlib's sense.

Main results

• TauCeti.IsRegularLocalRing.hasProjectiveDimensionLE: over a regular local ring of dimension at most n, every module has projective dimension at most n.
• TauCeti.IsRegularLocalRing.projectiveDimension_quotient_maximalIdeal_eq_ringKrullDim: the residue field of a regular local ring has projective dimension exactly the dimension of the ring.
• TauCeti.IsRegularLocalRing.globalDimension_eq_ringKrullDim: the global dimension of a regular local ring is its Krull dimension.
• TauCeti.IsRegularRing.hasProjectiveDimensionLE: over a regular ring of dimension at most n, every module has projective dimension at most n.
• ModuleCat.projectiveDimension_le_ringKrullDim: over a regular ring, the projective dimension of every module is at most the Krull dimension of the ring.
• TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE: a Noetherian local ring whose residue field has finite projective dimension is regular.
• TauCeti.isRegularLocalRing_iff_projectiveDimension_ne_top: a Noetherian local ring is regular exactly when its residue field has finite projective dimension.
• TauCeti.isRegularLocalRing_iff_globalDimension_lt_top: a Noetherian local ring is regular exactly when its global dimension is finite.
• TauCeti.isRegularLocalRing_tfae: Serre's characterization of regular local rings by the residue field, by the global dimension, and by the equalities gl dim R = dim R and pd κ = dim_κ 𝔪 / 𝔪².
• TauCeti.finrank_cotangentSpace_le_projectiveDimension_quotient_maximalIdeal: the residue field of a Noetherian local ring has projective dimension at least dim_κ 𝔪 / 𝔪².
• TauCeti.isRegularRing_of_globalDimension_lt_top: a Noetherian ring of finite global dimension is a regular ring.
• TauCeti.isRegularRing_of_isRegularLocalRing: a regular local ring is a regular ring, so its localizations at primes are regular local rings (an instance).
• TauCeti.IsRegularRing.projectiveDimension_le_ringKrullDim_of_faithfullyFlat: if a regular ring R is faithfully flat over a ring A, every finite A-module has projective dimension at most dim R.

Proof

For a finite module M over a regular local ring R of dimension d + 1, choose a parameter x ∈ 𝔪 \ 𝔪², so that R ⧸ (x) is regular of dimension d, and a finite free presentation 0 → N → P → M → 0. As R is a domain, x is regular on N ⊆ P. By induction N ⧸ x N has projective dimension at most d over R ⧸ (x), hence at most d + 1 over R by change of rings, while pd_R (N ⧸ x N) = pd_R N + 1. So pd_R N ≤ d and pd_R M ≤ d + 1. Cyclic modules are finite, and their projective dimensions bound those of all modules by Baer's criterion. For a regular ring the projective dimension of a finite module is the supremum of those of its localizations at maximal ideals, and these localizations are regular local rings of dimension at most that of the ring.

For the converse, induct on a bound n for the projective dimension of the residue field κ. If 𝔪 is an associated prime of R, a finite module of finite projective dimension is free, so κ is free and R is a field. Otherwise prime avoidance gives a nonzerodivisor x ∈ 𝔪 \ 𝔪². From 0 → 𝔪 → R → κ → 0, the projective dimension of 𝔪 is at most n - 1. As x is regular on 𝔪, the projective dimension of 𝔪 ⧸ x 𝔪 over R ⧸ (x) is also at most n - 1. The residue field of R ⧸ (x) is a direct summand of 𝔪 ⧸ x 𝔪, so R ⧸ (x) is regular by induction, and regularity lifts along the nonzerodivisor x (TauCeti.IsRegularLocalRing.of_quotient_nonZeroDivisor).

Along a faithfully flat map A → R, base change preserves the projective dimension of finite modules (ModuleCat.projectiveDimension_tensorProduct), so the bound over a regular ring R also bounds the finite A-modules. For a flat local homomorphism of Noetherian local rings and the residue field of A, this is the finite projective dimension from which Serre's characterization of regular local rings deduces that A is regular (H. Matsumura, Commutative Ring Theory, Theorem 23.7 (i)); see TauCeti.IsRegularLocalRing.of_faithfullyFlat and TauCeti.IsRegularLocalRing.of_flat_of_isLocalHom in Descent.lean.

References

• Stacks Project, Section 10.110, Rings of finite global dimension: Proposition 10.110.1 (00O7), Lemma 10.110.3 (00OA), Proposition 10.110.5 (00OC), Lemma 10.110.6 (0AFS) and Lemma 10.110.8 (00OE).
• Stacks Project, Lemma 10.109.12, reducing the global dimension to cyclic modules.
• H. Matsumura, Commutative Ring Theory, Section 19 (Regular rings), Theorem 19.2 for the converse.
• The names and shapes of the global-dimension criteria follow Nailin Guan's Mathlib pull request mathlib4#29802, Mathlib/RingTheory/RegularLocalRing/Localization.lean.

theorem TauCeti.IsRegularLocalRing.hasProjectiveDimensionLE_of_finite {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] {n : ℕ} (hn : ringKrullDim R ≤ ↑n) (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.HasProjectiveDimensionLE M n

Over a regular local ring of dimension at most n, every finite module has projective dimension at most n.

theorem TauCeti.IsRegularLocalRing.hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] {n : ℕ} (hn : ringKrullDim R ≤ ↑n) (M : ModuleCat R) : CategoryTheory.HasProjectiveDimensionLE M n

The global dimension of a regular local ring is at most its dimension. Over a regular local ring of dimension at most n, every module, finitely generated or not, has projective dimension at most n.

theorem TauCeti.IsRegularLocalRing.projectiveDimension_quotient_maximalIdeal_eq_ringKrullDim {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R)) = ringKrullDim R

The residue field of a regular local ring has projective dimension equal to the dimension of the ring. A minimal generating family of the maximal ideal is a regular sequence, whose quotient has projective dimension its length. Together with TauCeti.IsRegularLocalRing.hasProjectiveDimensionLE, the global dimension of a regular local ring is its Krull dimension.

theorem TauCeti.IsRegularLocalRing.globalDimension_eq_ringKrullDim {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] : globalDimension R = ringKrullDim R

The global dimension of a regular local ring is its Krull dimension. The upper bound is Stacks, Proposition 10.110.1 (00O7); the residue field attains it.

theorem TauCeti.IsRegularRing.hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsRegularRing R] [Small.{v, u} R] {n : ℕ} (hn : ringKrullDim R ≤ ↑n) (M : ModuleCat R) : CategoryTheory.HasProjectiveDimensionLE M n

The global dimension of a regular ring is at most its dimension. Over a regular ring of Krull dimension at most n, every module, finitely generated or not, has projective dimension at most n.

theorem ModuleCat.projectiveDimension_le_ringKrullDim {R : Type u} [CommRing R] [IsRegularRing R] [Small.{v, u} R] (M : ModuleCat R) : CategoryTheory.projectiveDimension M ≤ ringKrullDim R

Over a regular ring, the projective dimension of every module is at most the Krull dimension of the ring.

Serre's theorem: finite projective dimension of the residue field

theorem TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE (↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R))) n] : IsRegularLocalRing R

Serre's theorem. A Noetherian local ring whose residue field has finite projective dimension is a regular local ring. Its dimension is then that projective dimension, by TauCeti.IsRegularLocalRing.projectiveDimension_quotient_maximalIdeal_eq_ringKrullDim.

theorem TauCeti.isRegularLocalRing_iff_projectiveDimension_ne_top {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] : IsRegularLocalRing R ↔ CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R)) ≠ ⊤

A Noetherian local ring is regular exactly when its residue field has finite projective dimension.

theorem TauCeti.IsRegularLocalRing.globalDimension_lt_top {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] : globalDimension R < ⊤

A regular local ring has finite global dimension.

theorem TauCeti.IsRegularLocalRing.of_globalDimension_lt_top {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : globalDimension R < ⊤) : IsRegularLocalRing R

Serre's theorem, global dimension form. A Noetherian local ring of finite global dimension is a regular local ring: its residue field has finite projective dimension.

theorem TauCeti.isRegularLocalRing_iff_globalDimension_lt_top {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] : IsRegularLocalRing R ↔ globalDimension R < ⊤

A Noetherian local ring is regular exactly when its global dimension is finite. The global dimension is then the Krull dimension (TauCeti.IsRegularLocalRing.globalDimension_eq_ringKrullDim).

theorem TauCeti.isRegularLocalRing_tfae {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] : [CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R)) ≠ ⊤, globalDimension R < ⊤, IsRegularLocalRing R, globalDimension R = ringKrullDim R, CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R)) = ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R))].TFAE

Serre's characterization of regular local rings. For a Noetherian local ring R with residue field κ, the following are equivalent:

1. κ has finite projective dimension;
2. R has finite global dimension;
3. R is a regular local ring;
4. the global dimension of R is its Krull dimension;
5. the projective dimension of κ is dim_κ 𝔪 / 𝔪².

Conditions 4 and 5 are the equalities gl dim R = dim R and pd κ = dim_κ 𝔪 / 𝔪² of 00OC, which hold for a regular local ring; they are equivalent to regularity because R has finite Krull dimension.

theorem TauCeti.finrank_cotangentSpace_le_projectiveDimension_quotient_maximalIdeal {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] : ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) ≤ CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R))

The residue field of a Noetherian local ring has projective dimension at least dim_κ 𝔪 / 𝔪². When this projective dimension is finite, the ring is regular and the two are equal (TauCeti.isRegularLocalRing_tfae).

theorem TauCeti.isRegularRing_of_globalDimension_lt_top {R : Type u} [CommRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : globalDimension R < ⊤) : IsRegularRing R

A Noetherian ring of finite global dimension is a regular ring. Its localizations at primes have global dimension at most that of the ring, so they are regular local rings.

instance TauCeti.isRegularRing_of_isRegularLocalRing {R : Type u} [CommRing R] [IsRegularLocalRing R] : IsRegularRing R

A regular local ring is a regular ring: its localizations at all primes are regular local rings (Stacks, Lemma 10.110.6 (0AFS)). With Mathlib's instance IsRegularRing.isRegularLocalRing_localization, this makes Localization.AtPrime p a regular local ring for every prime p of a regular local ring. For any other localization S at p, use TauCeti.Excellence.mem_regularLocus_iff_of_isLocalization with TauCeti.Excellence.regularLocus_eq_univ.

theorem TauCeti.IsRegularRing.projectiveDimension_le_ringKrullDim_of_faithfullyFlat {A : Type w} [CommRing A] {R : Type u} [CommRing R] [Algebra A R] [Module.FaithfullyFlat A R] [IsRegularRing R] [Small.{v, w} A] (M : Type v) [AddCommGroup M] [Module A M] [Module.Finite A M] : CategoryTheory.projectiveDimension ↧M ≤ ringKrullDim R

If a regular ring R is faithfully flat over a ring A, every finite A-module has projective dimension at most dim R. Since a regular local ring is a regular ring (TauCeti.isRegularRing_of_isRegularLocalRing), this applies to a flat local homomorphism A → R of Noetherian local rings with R regular (Module.FaithfullyFlat.of_flat_of_isLocalHom).