Integral closures in reduced Artinian rings

Let R → E be a ring homomorphism with E reduced and Artinian, for instance a finite product of fields, and suppose R is integrally closed in E. Then R is normal in the sense of Stacks, Definition 10.37.11 (00GV): every localization of R at a prime is an integrally closed domain. Indeed, for a prime Q of R the localization E_Q of E at the image of R ∖ Q is again reduced and Artinian, and it is local: two distinct primes of E are separated by an idempotent, which is integral over R, hence comes from R, and so cannot lie over primes contained in Q. Thus E_Q is a field, and R_Q, which is integrally closed in E_Q, is an integrally closed domain.

This applies to the integral closure of any ring in a finite étale algebra over a field, a finite product of fields. It is the normality of the finite algebra attached to a finite étale cover of the punctured spectrum of a normal local domain, whose generic fibre is a finite étale algebra over the fraction field.

Main results

• IsIntegrallyClosedIn.isDomain_localization_atPrime and IsIntegrallyClosedIn.isIntegrallyClosed_localization_atPrime: a ring integrally closed in a reduced Artinian ring is normal.

References

• Stacks Project, Definition 10.37.11.
• Stacks Project, Lemma 58.20.3, whose proof uses the integral closure in the generic fibre of a finite étale cover of a punctured spectrum.
• The normality argument generalizes the étale case in T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Common/EtaleNormal.lean, where E is the generic fibre of an étale algebra over an integrally closed domain (eq_of_comap_le_of_etale and isField_localization_tensor_fractionRing_of_etale), as ported to TauCeti.RingTheory.Etale.Normal.

theorem IsIntegrallyClosedIn.isDomain_localization_atPrime {R : Type u_1} (E : Type u_2) [CommRing R] [CommRing E] [Algebra R E] [IsIntegrallyClosedIn R E] [IsArtinianRing E] [IsReduced E] (Q : Ideal R) [Q.IsPrime] : IsDomain (Localization.AtPrime Q)

A ring integrally closed in a reduced Artinian ring has domains as local rings. If R is integrally closed in a reduced Artinian ring E, for instance a finite product of fields, then every localization of R at a prime is a domain.

theorem IsIntegrallyClosedIn.isIntegrallyClosed_localization_atPrime {R : Type u_1} (E : Type u_2) [CommRing R] [CommRing E] [Algebra R E] [IsIntegrallyClosedIn R E] [IsArtinianRing E] [IsReduced E] (Q : Ideal R) [Q.IsPrime] : IsIntegrallyClosed (Localization.AtPrime Q)

A ring integrally closed in a reduced Artinian ring is normal. If R is integrally closed in a reduced Artinian ring E, for instance a finite product of fields, then every localization of R at a prime is integrally closed.