Depth of normal local domains

A Noetherian local domain R which is integrally closed and has dimension at least two has depth at least two. This is the local form of the (S₂) half of Serre's normality criterion (Stacks, Lemma 10.157.4 (031S)): a normal Noetherian ring satisfies (S₂). Consequently a Noetherian integrally closed local domain of dimension at most two is Cohen–Macaulay, which is the hypothesis miracle flatness asks of a two-dimensional normal local domain finite over a regular local ring.

Proof

The depth statement rests on the following property of the maximal ideal 𝔪: it is not an associated prime of R ⧸ (b), unless 𝔪 is principal. For b = 0 this holds because R is a domain and 𝔪 ≠ 0. For b ≠ 0, let 𝔪 c ⊆ (b) and put t = c / b in the fraction field, so that t 𝔪 ⊆ R. If t 𝔪 ⊆ 𝔪, then t is integral over R (Mathlib's isIntegral_of_smul_mem_submodule), hence lies in R, and c ∈ (b). Otherwise t u is a unit for some u ∈ 𝔪, and then 𝔪 = (u). A principal maximal ideal forces dimension at most one, so in dimension at least two, any nonzero x ∈ 𝔪 is followed by an element of 𝔪 regular on R ⧸ (x) (Mathlib's IsSMulRegular.subsingleton_linearMap_iff).

Main results

• TauCeti.IsIntegrallyClosed.mem_span_singleton_of_forall_mul_mem: in a Noetherian integrally closed local domain whose maximal ideal is not principal, 𝔪 c ⊆ (b) forces c ∈ (b).
• TauCeti.IsIntegrallyClosed.isSMulRegular_quotient_span_singleton_of_radical_span_pair: if (x, y) has maximal radical and the maximal ideal is nonprincipal, then y is regular on R ⧸ (x).
• IsLocalRing.two_le_depth_of_isIntegrallyClosed: a Noetherian integrally closed local domain of dimension at least two has depth at least two.
• Module.isCohenMacaulay_self_of_isIntegrallyClosed_of_krullDimLE_two: a Noetherian integrally closed local domain of dimension at most two is Cohen–Macaulay over itself.

References

• Stacks Project, Lemma 10.157.4, Serre's criterion for normality.
• H. Matsumura, Commutative Ring Theory, Theorem 23.8.

theorem TauCeti.IsIntegrallyClosed.mem_span_singleton_of_forall_mul_mem {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] (hm : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) {b c : R} (hc : ∀ z ∈ IsLocalRing.maximalIdeal R, z * c ∈ Ideal.span {b}) : c ∈ Ideal.span {b}

In a Noetherian integrally closed local domain whose maximal ideal is not principal, the maximal ideal is not an associated prime of R ⧸ (b): if z c ∈ (b) for every z in the maximal ideal, then c ∈ (b).

theorem TauCeti.IsIntegrallyClosed.isSMulRegular_quotient_span_singleton_of_radical_span_pair {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] (hm : ¬Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) {x y : R} (hxy : (Ideal.span {x, y}).radical = IsLocalRing.maximalIdeal R) : IsSMulRegular (R ⧸ Ideal.span {x}) y

In a Noetherian normal local domain with nonprincipal maximal ideal, if (x, y) has maximal radical, then y is a nonzerodivisor on R ⧸ (x).

theorem IsLocalRing.two_le_depth_of_isIntegrallyClosed {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] (hdim : 2 ≤ ringKrullDim R) : 2 ≤ depth ↧R

The (S₂) property of normal local domains. A Noetherian integrally closed local domain of dimension at least two has depth at least two. The local form of the (S₂) half of Serre's criterion, Stacks, Lemma 10.157.4 (031S).

theorem Module.isCohenMacaulay_self_of_isIntegrallyClosed_of_krullDimLE_two {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] [IsIntegrallyClosed R] [Ring.KrullDimLE 2 R] : IsCohenMacaulay R R

A Noetherian integrally closed local domain of dimension at most two is Cohen–Macaulay over itself.