Serre's criterion for normality

A Noetherian ring R is normal when every localization R_p at a prime is an integrally closed domain (Stacks, Definition 10.37.11 (00GV)). Serre's criterion says that this holds exactly when R satisfies (R_1) and (S_2): the local rings at primes of height at most one are regular, and depth R_p ≥ min (2, dim R_p) for every prime p (Stacks, Lemma 10.157.4 (031S)).

The forward direction is local: an integrally closed Noetherian local domain of dimension at most one is a field or a discrete valuation ring, hence regular, and one of dimension at least two has depth at least two (IsLocalRing.two_le_depth_of_isIntegrallyClosed).

For the converse, (S_2) forces every associated prime of R ⧸ (b), for a nonzerodivisor b, to have height one, and (R_1) makes the localization at such a prime a discrete valuation ring. If a / b is integral over R, it therefore lies in every such localization, so a ∈ (b): R is integrally closed in its total ring of fractions. Both conditions pass to the local rings R_p, which are reduced by (R_0) and (S_1) and hence domains (IsLocalRing.isDomain_of_isIntegrallyClosed).

Main results

• Module.SatisfiesSerreS.height_eq_one_of_isAssociatedPrime_quotient_span_singleton: in a Noetherian ring satisfying (S_2), the associated primes of R ⧸ (b) for a nonzerodivisor b have height one.
• TauCeti.isIntegrallyClosed_of_satisfiesSerreR_one_of_satisfiesSerreS_two: a Noetherian ring satisfying (R_1) and (S_2) is integrally closed in its total ring of fractions.
• TauCeti.satisfiesSerreR_one_of_forall_isIntegrallyClosed and TauCeti.satisfiesSerreS_two_of_forall_isIntegrallyClosed: a Noetherian normal ring satisfies (R_1) and (S_2).
• TauCeti.forall_isDomain_and_isIntegrallyClosed_iff_satisfiesSerreR_one_and_satisfiesSerreS_two: Serre's criterion, a Noetherian ring is normal if and only if it satisfies (R_1) and (S_2).

References

• Stacks Project, Lemma 10.157.4
• The proofs of Module.SatisfiesSerreS.height_eq_one_of_isAssociatedPrime_quotient_span_singleton and TauCeti.isIntegrallyClosed_of_satisfiesSerreR_one_of_satisfiesSerreS_two adapt the proof that regular rings are integrally closed from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit a39c3781b9850b9f3d5cbc9920322a3b8e365ef2 (Apache-2.0), lean/Pcf/Stacks/Common/RegularNormal.lean (Pcf.Stacks.isIntegrallyClosed_of_isRegularRing), with depth at least two in place of regularity and (R_1) in place of regularity in codimension one. That regular rings are integrally closed, TauCeti.IsRegularRing.isIntegrallyClosed, is now derived from these results.

theorem Module.SatisfiesSerreS.height_eq_one_of_isAssociatedPrime_quotient_span_singleton {R : Type u} [CommRing R] [IsNoetherianRing R] (h : SatisfiesSerreS 2 R R) {b : R} (hb : b ∈ nonZeroDivisors R) {P : Ideal R} (hP : IsAssociatedPrime P (R ⧸ Ideal.span {b})) : P.height = 1

Associated primes of a principal ideal under (S_2). In a Noetherian ring satisfying (S_2), every associated prime of R ⧸ (b), for a nonzerodivisor b, has height one.

theorem TauCeti.isIntegrallyClosed_of_satisfiesSerreR_one_of_satisfiesSerreS_two {R : Type u} [CommRing R] [IsNoetherianRing R] (hR : Ring.SatisfiesSerreR 1 R) (hS : Module.SatisfiesSerreS 2 R R) : IsIntegrallyClosed R

A Noetherian ring satisfying (R_1) and (S_2) is integrally closed in its total ring of fractions. Stacks, Lemma 10.157.4 (031S).

theorem TauCeti.satisfiesSerreR_one_of_forall_isIntegrallyClosed {R : Type u} [CommRing R] [IsNoetherianRing R] (h : ∀ (p : Ideal R) [inst : p.IsPrime], IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) : Ring.SatisfiesSerreR 1 R

The (R_1) half of Serre's criterion. A Noetherian ring whose local rings are integrally closed domains satisfies (R_1). Stacks, Lemma 10.157.4 (031S).

theorem TauCeti.satisfiesSerreS_two_of_forall_isIntegrallyClosed {R : Type u} [CommRing R] [IsNoetherianRing R] (h : ∀ (p : Ideal R) [inst : p.IsPrime], IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) : Module.SatisfiesSerreS 2 R R

The (S_2) half of Serre's criterion. A Noetherian ring whose local rings are integrally closed domains satisfies (S_2). Stacks, Lemma 10.157.4 (031S).

theorem TauCeti.forall_isDomain_and_isIntegrallyClosed_iff_satisfiesSerreR_one_and_satisfiesSerreS_two {R : Type u} [CommRing R] [IsNoetherianRing R] : (∀ (p : Ideal R) [inst : p.IsPrime], IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) ↔ Ring.SatisfiesSerreR 1 R ∧ Module.SatisfiesSerreS 2 R R

Serre's criterion for normality. A Noetherian ring is normal, that is, every localization at a prime is an integrally closed domain, if and only if it satisfies (R_1) and (S_2). Stacks, Lemma 10.157.4 (031S).