Integrally closed reduced local rings are domains

Mathlib's IsIntegrallyClosed R asks R to be integrally closed in its total ring of fractions FractionRing R, without assuming that R is a domain. This file shows that for a reduced Noetherian local ring this already forces R to be a domain: two minimal primes would split off a nontrivial idempotent of the total ring of fractions, which is integral over R but cannot lie in the local ring R (compare Stacks, Lemma 10.37.16 (030C)).

This is the step of Serre's criterion for normality which turns integral closedness in the total ring of fractions into the statement that every local ring is an integrally closed domain.

The idempotent is built from an element x ≠ 0 with x y = 0: the ideals J = ann x and I = ann J meet in zero, and I + J contains a nonzerodivisor b = i + j, so i / b is an idempotent of the total ring of fractions. Locality of R forces i = 0 or j = 0. The nonzerodivisor comes from Ideal.exists_mem_annihilator_sup_isSMulRegular.

Main results

• IsLocalRing.isDomain_of_isIntegrallyClosed: a reduced Noetherian local ring that is integrally closed in its total ring of fractions is a domain.

theorem IsLocalRing.isDomain_of_isIntegrallyClosed {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsReduced R] [IsIntegrallyClosed R] : IsDomain R

A reduced Noetherian local ring that is integrally closed in its total ring of fractions is a domain.