Regular rings are normal

A regular ring is integrally closed (Stacks, Lemma 10.157.5 (0567), whose "normal" means that every localization at a prime is an integrally closed domain). Consequently every localization of a regular ring at a prime is an integrally closed domain. This is the ring-level step of the statement that regular schemes are normal.

Proof

As in Stacks, this is an instance of Serre's criterion (R₁) + (S₂). A regular ring satisfies (R_n) for every n (IsRegularRing.satisfiesSerreR), and its local rings are regular, hence Cohen–Macaulay, so it satisfies (S_n) for every n (IsRegularRing.satisfiesSerreS). TauCeti.isIntegrallyClosed_of_satisfiesSerreR_one_of_satisfiesSerreS_two then shows that it is integrally closed in its total ring of fractions.

Main results

• TauCeti.IsRegularRing.isIntegrallyClosed: a regular ring is integrally closed. It is a low-priority instance, so with TauCeti.IsRegularRing.isRegularRing_localization and TauCeti.IsRegularLocalRing.isDomain every localization of a regular ring at a prime is found to be an integrally closed domain.

References

• Stacks Project, Lemma 10.157.5.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit a39c3781b9850b9f3d5cbc9920322a3b8e365ef2 (Apache-2.0), lean/Pcf/Stacks/Common/RegularNormal.lean: IsRegularRing.isIntegrallyClosed is its Pcf.Stacks.isIntegrallyClosed_of_isRegularRing. Its associated-prime argument now lives, with depth at least two in place of regularity, in TauCeti.RingTheory.SerreCondition.Normal.

@[instance 100]

instance TauCeti.IsRegularRing.isIntegrallyClosed (R : Type u_1) [CommRing R] [IsRegularRing R] : IsIntegrallyClosed R

A regular ring is integrally closed (Stacks, Lemma 10.157.5 (0567)): it satisfies (R_1) and (S_2), so Serre's criterion applies.