Normality along étale homomorphisms

For an étale homomorphism of local rings A → B, that is, B is the localization at a prime of an étale A-algebra and A → B is local, A is a normal domain (a domain that is integrally closed) if and only if B is (Stacks, Proposition 41.19.7 (025P)).

The statements need no Noetherian, depth or dimension hypotheses.

Main results

• TauCeti.Algebra.Etale.isDomain_localization_atPrime_of_isIntegrallyClosed and isIntegrallyClosed_localization_atPrime_of_isIntegrallyClosed: the local rings of an étale algebra over an integrally closed domain are integrally closed domains. The algebra is integrally closed in its generic fibre, a reduced Artinian ring, so this is a case of IsIntegrallyClosedIn.isDomain_localization_atPrime.
• TauCeti.Algebra.Etale.isDomain_localization_atPrime_of_localization_under and isIntegrallyClosed_localization_atPrime_of_localization_under: for A → S étale and a prime q of S over p, if A_p is an integrally closed domain then so is S_q.
• TauCeti.Algebra.IsEtaleAt.isDomain_localization_atPrime_of_localization_under and isIntegrallyClosed_localization_atPrime_of_localization_under: the same when S is only finitely presented and étale at q, since then some S_f with f ∉ q is étale.
• TauCeti.Algebra.Etale.isIntegrallyClosed: an étale domain over an integrally closed domain is integrally closed.
• TauCeti.Algebra.isNormalDomain_iff_of_etale: Stacks 025P; normality is expressed by IsDomain and IsIntegrallyClosed since Mathlib has no predicate "normal domain".

References

• Stacks Project, Proposition 41.19.7 and Lemma 10.163.9.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Common/EtaleNormal.lean, which proves the ascent: Algebra.Etale.isDomain_localization_atPrime_of_isIntegrallyClosed and isIntegrallyClosed_localization_atPrime_of_isIntegrallyClosed are its Pcf.Stacks.isDomain_isIntegrallyClosed_atPrime_of_etale_of_isDomain (whose private steps eq_of_comap_le_of_etale and isField_localization_tensor_fractionRing_of_etale are generalized in TauCeti.RingTheory.IntegralClosure.ReducedArtinian); Algebra.Etale.isDomain_localization_atPrime_of_localization_under and isIntegrallyClosed_localization_atPrime_of_localization_under are its Pcf.Stacks.isDomain_isIntegrallyClosed_atPrime_of_etale; and Algebra.Etale.isIntegrallyClosed is its Pcf.Stacks.isIntegrallyClosed_of_etale, which the source states through its own normal-ring predicate. The descent direction and isNormalDomain_iff_of_etale are new.

theorem TauCeti.Algebra.Etale.isDomain_localization_atPrime_of_isIntegrallyClosed (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [Algebra.Etale R S] (Q : Ideal S) [Q.IsPrime] : IsDomain (Localization.AtPrime Q)

The local rings of an étale algebra over an integrally closed domain are domains. The étale case of Stacks, Lemma 10.163.9 (033C), at one prime.

theorem TauCeti.Algebra.Etale.isIntegrallyClosed_localization_atPrime_of_isIntegrallyClosed (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [Algebra.Etale R S] (Q : Ideal S) [Q.IsPrime] : IsIntegrallyClosed (Localization.AtPrime Q)

The local rings of an étale algebra over an integrally closed domain are integrally closed. The étale case of Stacks, Lemma 10.163.9 (033C), at one prime.

theorem TauCeti.Algebra.Etale.isDomain_localization_atPrime_of_localization_under (A : Type u_1) {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [Algebra.Etale A S] (q : Ideal S) [q.IsPrime] [IsDomain (Localization.AtPrime (Ideal.under A q))] [IsIntegrallyClosed (Localization.AtPrime (Ideal.under A q))] : IsDomain (Localization.AtPrime q)

Local rings of an étale algebra over integrally closed local rings of the base are domains. Let A → S be étale and q a prime of S over p. If A_p is an integrally closed domain, then S_q is a domain. The étale case of Stacks, Lemma 10.163.9 (033C), in local form.

theorem TauCeti.Algebra.Etale.isIntegrallyClosed_localization_atPrime_of_localization_under (A : Type u_1) {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [Algebra.Etale A S] (q : Ideal S) [q.IsPrime] [IsDomain (Localization.AtPrime (Ideal.under A q))] [IsIntegrallyClosed (Localization.AtPrime (Ideal.under A q))] : IsIntegrallyClosed (Localization.AtPrime q)

Integrally closed local rings ascend along étale maps. Let A → S be étale and q a prime of S over p. If A_p is an integrally closed domain, then S_q is integrally closed. The étale case of Stacks, Lemma 10.163.9 (033C), in local form.

theorem TauCeti.Algebra.Etale.isIntegrallyClosed (A : Type u_1) (S : Type u_2) [CommRing A] [CommRing S] [Algebra A S] [Algebra.Etale A S] [IsDomain A] [IsIntegrallyClosed A] [IsDomain S] : IsIntegrallyClosed S

An étale domain over an integrally closed domain is integrally closed. The étale case of Stacks, Lemma 10.163.9 (033C), for domains.

theorem TauCeti.Algebra.IsEtaleAt.isDomain_localization_atPrime_of_localization_under (A : Type u_1) {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [Algebra.FinitePresentation A S] (q : Ideal S) [q.IsPrime] [Algebra.IsEtaleAt A q] [IsDomain (Localization.AtPrime (Ideal.under A q))] [IsIntegrallyClosed (Localization.AtPrime (Ideal.under A q))] : IsDomain (Localization.AtPrime q)

Local rings at étale points are domains. Let S be finitely presented over A and étale at a prime q over p. If A_p is an integrally closed domain, then S_q is a domain. The pointwise étale case of Stacks, Lemma 10.163.9 (033C), in local form.

theorem TauCeti.Algebra.IsEtaleAt.isIntegrallyClosed_localization_atPrime_of_localization_under (A : Type u_1) {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] [Algebra.FinitePresentation A S] (q : Ideal S) [q.IsPrime] [Algebra.IsEtaleAt A q] [IsDomain (Localization.AtPrime (Ideal.under A q))] [IsIntegrallyClosed (Localization.AtPrime (Ideal.under A q))] : IsIntegrallyClosed (Localization.AtPrime q)

Local rings at étale points are integrally closed. Let S be finitely presented over A and étale at a prime q over p. If A_p is an integrally closed domain, then S_q is integrally closed. The pointwise étale case of Stacks, Lemma 10.163.9 (033C), in local form.

theorem TauCeti.Algebra.isNormalDomain_iff_of_etale {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [CommRing B] [CommRing C] [IsLocalRing A] [Algebra A B] [IsLocalHom (algebraMap A B)] [Algebra A C] [Algebra.Etale A C] (q : Ideal C) [q.IsPrime] (e : B ≃ₐ[A] Localization.AtPrime q) : IsDomain A ∧ IsIntegrallyClosed A ↔ IsDomain B ∧ IsIntegrallyClosed B

Normality along étale homomorphisms of local rings. Let A be a local ring, C an étale A-algebra, q a prime of C, and B an A-algebra isomorphic to C_q with A → B local (an étale homomorphism of local rings, Stacks, Definition 41.11.1 (0258)). Then A is an integrally closed domain iff B is. Stacks, Proposition 41.19.7 (025P); Stacks assumes A and B Noetherian, and no Noetherian hypothesis is assumed here.