Support dimension of a localized module

Let M be a finite module over a Noetherian ring R and p a prime containing the annihilator of M. The support of the localization M_p over R_p is zero-dimensional exactly when p is a minimal prime of the support of M. Primes of the support of M_p contract to primes of the support of M below p, and a minimal prime strictly below p is associated to M, so it survives in M_p as a non-maximal associated prime.

This is the dimension input to the characterization of Serre's condition (S_1) as the absence of embedded primes.

Main results

• Module.exists_supportDim_eq_natCast: a nonzero module over a ring of finite Krull dimension, such as a Noetherian local ring, has support of finite dimension.
• Module.supportDim_localizedModule_nonpos_iff: M_p has zero-dimensional support exactly when p is a minimal prime of the support of M.

theorem Module.exists_supportDim_eq_natCast {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [FiniteRingKrullDim R] [Nontrivial M] : ∃ (k : ℕ), supportDim R M = ↑k

The support of a nonzero module over a ring of finite Krull dimension, such as a Noetherian local ring, has finite dimension: it is neither ⊥ nor ⊤.

theorem Module.supportDim_localizedModule_nonpos_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] {p : Ideal R} [p.IsPrime] (hp : annihilator R M ≤ p) : supportDim (Localization.AtPrime p) (LocalizedModule p.primeCompl M) ≤ 0 ↔ p ∈ (annihilator R M).minimalPrimes

Let M be a finite module over a Noetherian ring and p a prime containing the annihilator of M. The support of M_p has dimension zero exactly when p is a minimal prime of the support of M.