Serre's conditions (S_n) and (R_n)

Let R be a Noetherian ring. A finite R-module M satisfies Serre's condition (S_n) if depth M_p ≥ min (n, dim Supp M_p) for every prime p of R, and R satisfies (R_n) if the local ring R_p is regular for every prime p of height at most n (Stacks, Definition 10.157.1 (031P)). These are the two halves of Serre's criterion for normality, (R_1) + (S_2), and the depth condition (S_2) is what lets sections of a module extend across closed subsets of codimension at least two. Serre's criterion itself is proved in TauCeti.RingTheory.SerreCondition.Normal.

Depth is Mathlib's IsLocalRing.depth and the dimension of the support is Mathlib's Module.supportDim. The zero module has depth ⊤ and support dimension ⊥, so a prime outside the support of M imposes no condition.

Main definitions

• Module.SatisfiesSerreS n R M: the R-module M satisfies (S_n).
• Ring.SatisfiesSerreR n R: every prime of R of height at most n lies in the regular locus TauCeti.Excellence.regularLocus R.

Main results

• Module.satisfiesSerreS_zero and Module.SatisfiesSerreS.mono: every module satisfies (S_0), and (S_n) implies (S_m) for m ≤ n; likewise Ring.SatisfiesSerreR.mono, and a regular ring satisfies (R_n) and (S_n) for every n (IsRegularRing.satisfiesSerreR and IsRegularRing.satisfiesSerreS).
• Module.satisfiesSerreS_self_iff: a ring satisfies (S_n) as a module over itself exactly when depth R_p ≥ min (n, dim R_p) for every prime p.
• Module.SatisfiesSerreS.localization_self and Ring.SatisfiesSerreR.localization: for the ring itself, (S_n) and (R_n) pass to every localization, whose local rings are local rings of R.
• Module.forall_satisfiesSerreS_iff_forall_isCohenMacaulay: a finite module satisfies (S_n) for every n if and only if all of its localizations at primes are Cohen–Macaulay; in particular a finite Cohen–Macaulay module over a Noetherian local ring satisfies every (S_n) (Module.IsCohenMacaulay.satisfiesSerreS).
• Module.satisfiesSerreS_one_iff: a finite module satisfies (S_1) if and only if it has no embedded primes, that is, its associated primes are the minimal primes of its support (Stacks, Lemma 10.157.2 (031Q)).
• TauCeti.isReduced_iff_satisfiesSerreR_zero_and_satisfiesSerreS_one: a Noetherian ring is reduced if and only if it satisfies (R_0) and (S_1) (Stacks, Lemma 10.157.3 (031R)); the forward half of (R_0) is IsReduced.satisfiesSerreR_zero, which needs no Noetherian hypothesis.

The dimension input to Module.satisfiesSerreS_one_iff is Module.supportDim_localizedModule_nonpos_iff, in TauCeti.RingTheory.KrullDimension.Module: M_p has zero-dimensional support exactly when p is a minimal prime of the support of M.

References

• Stacks Project, Section 10.157

def Module.SatisfiesSerreS (n : ℕ) (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M] : Prop

An R-module M satisfies Serre's condition (S_n) if for every prime p of R the depth of M_p over R_p is at least min (n, dim Supp M_p). This is meant for finite modules over a Noetherian ring. Since the zero module has depth ⊤, primes outside the support impose nothing. Stacks, Definition 10.157.1 (031P).

theorem Module.satisfiesSerreS_iff {n : ℕ} {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] : SatisfiesSerreS n R M ↔ ∀ (p : Ideal R) [inst : p.IsPrime], min (↑n) (supportDim (Localization.AtPrime p) (LocalizedModule p.primeCompl M)) ≤ ↑(IsLocalRing.depth ↧(LocalizedModule p.primeCompl M))

Unfolds Module.SatisfiesSerreS.

@[simp]

theorem Module.satisfiesSerreS_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] : SatisfiesSerreS 0 R M

Every module satisfies (S_0).

@[simp]

theorem Module.satisfiesSerreS_of_subsingleton {n : ℕ} {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] : SatisfiesSerreS n R M

The zero module satisfies (S_n) for every n.

theorem Module.SatisfiesSerreS.mono {n : ℕ} {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {m : ℕ} (h : SatisfiesSerreS n R M) (hmn : m ≤ n) : SatisfiesSerreS m R M

Serre's condition (S_n) implies (S_m) for m ≤ n.

theorem Module.forall_satisfiesSerreS_iff_forall_isCohenMacaulay {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : (∀ (n : ℕ), SatisfiesSerreS n R M) ↔ ∀ (p : Ideal R) [inst : p.IsPrime], IsCohenMacaulay (Localization.AtPrime p) (LocalizedModule p.primeCompl M)

A finite module over a Noetherian ring satisfies (S_n) for every n if and only if its localization at every prime is Cohen–Macaulay.

theorem Module.IsCohenMacaulay.satisfiesSerreS {n : ℕ} {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] [Module.Finite R M] (h : IsCohenMacaulay R M) : SatisfiesSerreS n R M

A finite Cohen–Macaulay module over a Noetherian local ring satisfies (S_n) for every n, since its localizations at primes are Cohen–Macaulay (Module.IsCohenMacaulay.localizedModule).

theorem Module.satisfiesSerreS_one_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : SatisfiesSerreS 1 R M ↔ associatedPrimes R M = (annihilator R M).minimalPrimes

A finite module over a Noetherian ring satisfies (S_1) if and only if it has no embedded primes: its associated primes are exactly the minimal primes of its support. Stacks, Lemma 10.157.2 (031Q).

theorem Module.satisfiesSerreS_self_iff {n : ℕ} {R : Type u} [CommRing R] : SatisfiesSerreS n R R ↔ ∀ (p : Ideal R) [inst : p.IsPrime], min (↑n) (ringKrullDim (Localization.AtPrime p)) ≤ ↑(IsLocalRing.depth ↧(Localization.AtPrime p))

For the ring itself, Serre's condition (S_n) compares the depth of each local ring R_p with its dimension: R satisfies (S_n) exactly when depth R_p ≥ min (n, dim R_p) for every prime p of R.

theorem Module.SatisfiesSerreS.localization_self {n : ℕ} {R : Type u} [CommRing R] [IsNoetherianRing R] (h : SatisfiesSerreS n R R) (T : Submonoid R) (S : Type u_1) [CommRing S] [Algebra R S] [IsLocalization T S] : SatisfiesSerreS n S S

Serre's condition (S_n) for a Noetherian ring passes to its localizations: the local rings of a localization S of R are local rings of R.

def Ring.SatisfiesSerreR (n : ℕ) (R : Type u) [CommRing R] : Prop

A ring R satisfies Serre's condition (R_n) if every prime of height at most n lies in the regular locus, that is, R_p is a regular local ring whenever ht p ≤ n. Stacks, Definition 10.157.1 (031P).

theorem Ring.satisfiesSerreR_iff {n : ℕ} {R : Type u} [CommRing R] : SatisfiesSerreR n R ↔ ∀ (p : Ideal R) [inst : p.IsPrime], p.height ≤ ↑n → IsRegularLocalRing (Localization.AtPrime p)

Restates Ring.SatisfiesSerreR in terms of the localizations at primes.

theorem Ring.SatisfiesSerreR.mono {n : ℕ} {R : Type u} [CommRing R] {m : ℕ} (h : SatisfiesSerreR n R) (hmn : m ≤ n) : SatisfiesSerreR m R

Serre's condition (R_n) implies (R_m) for m ≤ n.

theorem Ring.SatisfiesSerreR.localization {n : ℕ} {R : Type u} [CommRing R] (h : SatisfiesSerreR n R) (T : Submonoid R) (S : Type u_1) [CommRing S] [Algebra R S] [IsLocalization T S] : SatisfiesSerreR n S

Serre's condition (R_n) passes to localizations: a prime of a localization S of R has the same height as its contraction to R, and the same local ring.

theorem IsRegularRing.satisfiesSerreR {R : Type u} [CommRing R] [IsRegularRing R] (n : ℕ) : Ring.SatisfiesSerreR n R

A regular ring satisfies (R_n) for every n.

theorem IsRegularRing.satisfiesSerreS {R : Type u} [CommRing R] [IsRegularRing R] (n : ℕ) : Module.SatisfiesSerreS n R R

A regular ring satisfies (S_n) for every n: its local rings are regular, hence Cohen–Macaulay, so their depth equals their dimension.

theorem IsReduced.satisfiesSerreR_zero {R : Type u} [CommRing R] [IsReduced R] : Ring.SatisfiesSerreR 0 R

A reduced ring satisfies (R_0): its localizations at minimal primes are fields.

theorem TauCeti.isReduced_iff_satisfiesSerreR_zero_and_satisfiesSerreS_one {R : Type u} [CommRing R] [IsNoetherianRing R] : IsReduced R ↔ Ring.SatisfiesSerreR 0 R ∧ Module.SatisfiesSerreS 1 R R

A Noetherian ring is reduced if and only if it satisfies (R_0) and (S_1): its localizations at minimal primes are fields and it has no embedded primes. Stacks, Lemma 10.157.3 (031R).