Projective dimension along the quotient by a nonzerodivisor

Let x be a nonzerodivisor of a commutative ring R. A module L over R ⧸ (x) is also an R-module, and its projective dimension grows by at most one:

pd_R L ≤ pd_{R ⧸ (x)} L + 1.

In the other direction, reducing an R-module M on which x is regular does not increase the projective dimension:

pd_{R ⧸ (x)} (M ⧸ x M) ≤ pd_R M.

A projective R ⧸ (x)-module is a retract of G ⧸ x G for a projective R-module G, and 0 → G → G → G ⧸ x G → 0, the first map being multiplication by x, shows that G ⧸ x G has projective dimension at most one over R. Dimension shifting along a projective presentation over R ⧸ (x) then gives the bound in general, because restriction of scalars is exact.

This is the change-of-rings step in the induction proving that every module over a regular local ring of dimension d has projective dimension at most d: there x is a parameter and R ⧸ (x) is regular of dimension d - 1.

When x is not a unit, the module R ⧸ (x) attains the first bound: it is projective over R ⧸ (x), and it has projective dimension exactly one over R because it is not flat, hence not projective.

For the reduction, a projective presentation 0 → K → P → M → 0 stays short exact modulo x, because x is regular on M; the reduction of the projective module P is projective over R ⧸ (x), and x is again regular on K ⊆ P, so induction on the projective dimension applies. This is the change-of-rings step in Serre's theorem that a Noetherian local ring whose residue field has finite projective dimension is regular.

Main results

• ModuleCat.hasProjectiveDimensionLT_restrictScalars_of_projective: a projective R ⧸ (x)-module has projective dimension at most one over R.
• ModuleCat.hasProjectiveDimensionLE_restrictScalars_quotient: if an R ⧸ (x)-module has projective dimension at most n, then it has projective dimension at most n + 1 over R.
• ModuleCat.hasProjectiveDimensionLE_of_isScalarTower_quotient: the same bound for an R-module carrying a compatible R ⧸ (x)-module structure.
• ModuleCat.projectiveDimension_quotient_span_singleton_eq_one: if x is not a unit, then R ⧸ (x) has projective dimension exactly one over R.
• ModuleCat.hasProjectiveDimensionLE_quotient_smul_top: if x is regular on an R-module M of projective dimension at most n, then M ⧸ x M has projective dimension at most n over R ⧸ (x).

No finiteness or locality is assumed: the bounds hold for all modules.

References

• H. Matsumura, Commutative Ring Theory, Section 19, the lemmas preceding Theorem 19.2.

theorem ModuleCat.hasProjectiveDimensionLT_restrictScalars_of_projective {R : Type u} [CommRing R] [Small.{v, u} R] {x : R} (hx : x ∈ nonZeroDivisors R) (P : ModuleCat (R ⧸ Ideal.span {x})) [CategoryTheory.Projective P] : CategoryTheory.HasProjectiveDimensionLT ((restrictScalars (Ideal.Quotient.mk (Ideal.span {x}))).obj P) 2

A projective module over R ⧸ (x), for a nonzerodivisor x, has projective dimension at most one over R.

theorem ModuleCat.hasProjectiveDimensionLE_restrictScalars_quotient {R : Type u} [CommRing R] [Small.{v, u} R] {x : R} (hx : x ∈ nonZeroDivisors R) (n : ℕ) (L : ModuleCat (R ⧸ Ideal.span {x})) [CategoryTheory.HasProjectiveDimensionLE L n] : CategoryTheory.HasProjectiveDimensionLE ((restrictScalars (Ideal.Quotient.mk (Ideal.span {x}))).obj L) (n + 1)

Change of rings for projective dimension. If x is a nonzerodivisor of R and an R ⧸ (x)-module L has projective dimension at most n, then L has projective dimension at most n + 1 as an R-module.

theorem ModuleCat.hasProjectiveDimensionLE_of_isScalarTower_quotient {R : Type u} [CommRing R] [Small.{v, u} R] {x : R} (hx : x ∈ nonZeroDivisors R) (n : ℕ) (L : Type v) [AddCommGroup L] [Module R L] [Module (R ⧸ Ideal.span {x}) L] [IsScalarTower R (R ⧸ Ideal.span {x}) L] [CategoryTheory.HasProjectiveDimensionLE (↧L) n] : CategoryTheory.HasProjectiveDimensionLE (↧L) (n + 1)

Change of rings for projective dimension, for an R-module with a compatible R ⧸ (x)-module structure: if its projective dimension over R ⧸ (x) is at most n, then its projective dimension over R is at most n + 1.

theorem ModuleCat.projectiveDimension_quotient_span_singleton_eq_one {R : Type u} [CommRing R] [Small.{v, u} R] {x : R} (hx : x ∈ nonZeroDivisors R) (hx' : ¬IsUnit x) : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ Ideal.span {x})) = 1

The quotient R ⧸ (x) by a nonzerodivisor x that is not a unit has projective dimension exactly one over R: it is free over R ⧸ (x), and it is not flat over R.

theorem ModuleCat.hasProjectiveDimensionLE_quotient_smul_top {R : Type u} [CommRing R] [Small.{v, u} R] {x : R} (hx : x ∈ nonZeroDivisors R) (n : ℕ) (M : ModuleCat R) (hM : IsSMulRegular (↑M) x) [CategoryTheory.HasProjectiveDimensionLE M n] : CategoryTheory.HasProjectiveDimensionLE (↧(↑M ⧸ Ideal.span {x} • ⊤)) n

Change of rings for projective dimension, by reduction. If x is a nonzerodivisor of R which is regular on an R-module M of projective dimension at most n, then M ⧸ x M has projective dimension at most n over R ⧸ (x).