The Auslander–Buchsbaum formula

Let M be a nonzero finite module of finite projective dimension over a Noetherian local ring R. The Auslander–Buchsbaum formula states projectiveDimension M + depth M = depth R.

Applied to the residue field κ = R ⧸ 𝔪, whose depth is zero, it shows that if κ has finite projective dimension, then that dimension is depth R, hence at most dim R. This is the upper bound in Serre's characterization of regular local rings by finite global dimension.

Main results

• ModuleCat.projectiveDimension_add_depth_eq_depth: the Auslander–Buchsbaum formula (Stacks, Proposition 10.111.1 (090V)).
• IsLocalRing.projectiveDimension_quotient_maximalIdeal_eq_depth: a residue field of finite projective dimension has projective dimension depth R.
• IsLocalRing.projectiveDimension_quotient_maximalIdeal_le_ringKrullDim: a residue field of finite projective dimension has projective dimension at most dim R (Stacks, Lemma 10.110.4 (00OB)).

Proof

Induction on p = projectiveDimension M. If p = 0, then M is projective, hence free, and a nonzero finite free module has the depth of R. If p > 0, choose a minimal free presentation 0 → K → F → M → 0, with K ⊆ 𝔪 F; then K has projective dimension p - 1, so depth K + (p - 1) = depth R by induction. The depth inequalities for short exact sequences give depth K - 1 ≤ depth M. For the reverse inequality depth M + 1 ≤ depth K:

• if p ≥ 2, then depth K < depth R = depth F, and the depth inequalities suffice;
• if p = 1, then K is free, and the inclusion K → F has image in 𝔪 F, so it induces zero on Ext (R ⧸ 𝔪) - n; the long exact sequence then shows that every connecting map Ext (R ⧸ 𝔪) M n → Ext (R ⧸ 𝔪) K (n + 1) is surjective.

References

• Stacks Project, Proposition 10.111.1.
• Stacks Project, Lemma 10.110.4.
• W. Bruns, J. Herzog, Cohen–Macaulay rings, Theorem 1.3.3.

theorem ModuleCat.projectiveDimension_add_depth_eq_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] (hM : CategoryTheory.projectiveDimension M ≠ ⊤) : CategoryTheory.projectiveDimension M + ↑(IsLocalRing.depth M) = ↑(IsLocalRing.depth ↧R)

The Auslander–Buchsbaum formula. For a nonzero finite module M of finite projective dimension over a Noetherian local ring R, projectiveDimension M + depth M = depth R. Stacks, Proposition 10.111.1 (090V).

theorem IsLocalRing.projectiveDimension_quotient_maximalIdeal_eq_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ maximalIdeal R)) ≠ ⊤) : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ maximalIdeal R)) = ↑(depth ↧R)

If the residue field κ of a Noetherian local ring R has finite projective dimension, that dimension is depth R.

theorem IsLocalRing.projectiveDimension_quotient_maximalIdeal_le_ringKrullDim {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ maximalIdeal R)) ≠ ⊤) : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ maximalIdeal R)) ≤ ringKrullDim R

If the residue field κ of a Noetherian local ring R has finite projective dimension, that dimension is at most the Krull dimension of R. Stacks, Lemma 10.110.4 (00OB).