Projective dimension over a local ring

Let R be a Noetherian local ring whose maximal ideal 𝔪 is an associated prime of R, that is, of depth zero: some nonzero s ∈ R satisfies 𝔪 s = 0. Then every finite R-module of finite projective dimension is free. This is the depth-zero case of the Auslander–Buchsbaum formula pd M + depth M = depth R.

The embedding κ → R, 1 ↦ s, of the residue field stays injective after tensoring with a flat module, so κ ⊗ - preserves injectivity of maps out of flat modules. For a presentation 0 → K → F → M → 0 with F finite free and K free by induction on the projective dimension, κ ⊗ K → κ ⊗ F is therefore injective, and M is free by Nakayama's lemma.

This is the base case of Serre's theorem that a Noetherian local ring whose residue field has finite projective dimension is regular. The induction step is a change of rings for the residue field: for a nonzerodivisor x ∈ 𝔪 \ 𝔪², the residue field of R ⧸ (x) is a direct summand of 𝔪 ⧸ x 𝔪, so a bound n + 1 for the projective dimension of the residue field of R gives the bound n for that of R ⧸ (x).

In the other direction, the projective dimension of the residue field κ of any Noetherian local ring is at least the embedding dimension dim_κ 𝔪/𝔪² (Stacks 00OA). Lift a basis of 𝔪/𝔪² to x₁, …, xₙ ∈ 𝔪 and compare the Koszul complex K(x) with a minimal finite free resolution F of κ of length d along a chain map over κ. The comparison stays injective modulo 𝔪 in every degree, and Kₙ = ⋀ⁿ Rⁿ ≅ R is nonzero modulo 𝔪, so Fₙ ≠ 0 and n ≤ d. Neither exactness of K(x) nor regularity of R is used.

Main results

• LinearMap.lTensor_residueField_injective_of_maximalIdeal_mem_associatedPrimes: over a local ring of depth zero, κ ⊗ - preserves injectivity of linear maps out of flat modules.
• Module.free_of_hasProjectiveDimensionLE_of_maximalIdeal_mem_associatedPrimes: over a Noetherian local ring of depth zero, a finite module of finite projective dimension is free.
• TauCeti.IsLocalRing.hasProjectiveDimensionLE_residueField_quotient: for a nonzerodivisor x ∈ 𝔪 \ 𝔪², if the residue field of R has projective dimension at most n + 1, then the residue field of R ⧸ (x) has projective dimension at most n over R ⧸ (x).
• TauCeti.IsLocalRing.finrank_cotangentSpace_le_of_hasProjectiveDimensionLE and TauCeti.IsLocalRing.finrank_cotangentSpace_le_projectiveDimension_quotient_maximalIdeal: the residue field of a Noetherian local ring has projective dimension at least dim_κ 𝔪/𝔪² (Stacks 00OA).

References

• H. Matsumura, Commutative Ring Theory, Theorem 19.1 (the Auslander–Buchsbaum formula) and the proof of Theorem 19.2.
• The Stacks Project, Lemma 10.110.3, the lower bound by the embedding dimension, via Koszul complexes and minimal resolutions.

theorem LinearMap.lTensor_residueField_injective_of_maximalIdeal_mem_associatedPrimes {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hm : IsLocalRing.maximalIdeal R ∈ associatedPrimes R R) {K : Type u_1} {F : Type u_2} [AddCommGroup K] [Module R K] [Module.Flat R K] [AddCommGroup F] [Module R F] {l : K →ₗ[R] F} (hl : Function.Injective ⇑l) : Function.Injective ⇑(lTensor (IsLocalRing.ResidueField R) l)

Over a local ring whose maximal ideal is an associated prime, tensoring with the residue field preserves injectivity of linear maps out of flat modules.

theorem Module.free_of_hasProjectiveDimensionLE_of_maximalIdeal_mem_associatedPrimes {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (hm : IsLocalRing.maximalIdeal R ∈ associatedPrimes R R) (n : ℕ) (M : ModuleCat R) [Module.Finite R ↑M] [CategoryTheory.HasProjectiveDimensionLE M n] : Free R ↑M

Finite projective dimension in depth zero. Over a Noetherian local ring whose maximal ideal is an associated prime, a finite module of finite projective dimension is free.

theorem TauCeti.IsLocalRing.hasProjectiveDimensionLE_residueField_quotient {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {n : ℕ} {x : R} (hxm : x ∈ IsLocalRing.maximalIdeal R) (hx2 : x ∉ IsLocalRing.maximalIdeal R ^ 2) (hx : x ∈ nonZeroDivisors R) [IsLocalRing (R ⧸ Ideal.span {x})] [Small.{v, u} (R ⧸ Ideal.span {x})] [CategoryTheory.HasProjectiveDimensionLE (↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R))) (n + 1)] : CategoryTheory.HasProjectiveDimensionLE (↧(Shrink.{v, u} ((R ⧸ Ideal.span {x}) ⧸ IsLocalRing.maximalIdeal (R ⧸ Ideal.span {x})))) n

Change of rings for the residue field. If the residue field of a local ring R has projective dimension at most n + 1 and x ∈ 𝔪 \ 𝔪² is a nonzerodivisor, then the residue field of R ⧸ (x) has projective dimension at most n over R ⧸ (x). Indeed 𝔪 has projective dimension at most n, hence so does 𝔪 ⧸ x 𝔪 over R ⧸ (x), and the residue field of R ⧸ (x) is a direct summand of 𝔪 ⧸ x 𝔪. This is the induction step of Serre's theorem.

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

The projective dimension of the residue field bounds the embedding dimension (Stacks, Lemma 10.110.3 (00OA)). If the residue field κ of a Noetherian local ring R has projective dimension at most d, then dim_κ 𝔪/𝔪² ≤ d.

theorem TauCeti.IsLocalRing.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 projective dimension of the residue field is at least the embedding dimension (Stacks, Lemma 10.110.3 (00OA)): for a Noetherian local ring R with residue field κ, dim_κ 𝔪/𝔪² ≤ pd_R κ.