Étaleness at a prime: flatness and unramifiedness of the local ring

Let S be a finitely presented R-algebra and q a prime of S. Mathlib's Algebra.IsEtaleAt R q asks that S_q be formally étale over R. This file shows that this is exactly flatness of S_q over R together with Mathlib's Algebra.IsUnramifiedAt R q (Algebra.isEtaleAt_iff_flat_and_isUnramifiedAt). Only flatness at the single prime q is assumed; Mathlib's Algebra.IsEtaleAt.of_isUnramifiedAt_of_flat asks for flatness of all of S.

The forward direction spreads étaleness to some S_f with f ∉ q (Algebra.exists_etale_of_isEtaleAt), which is flat, and localizes. For the reverse direction, put p = q ∩ R. The local ring S_q is flat over R_p, and its closed fibre κ(p) ⊗[R_p] S_q is formally unramified and essentially of finite type over the field κ(p), hence formally étale. Mathlib's local criterion Algebra.FormallySmooth.of_formallySmooth_residueField_tensor then makes S_q formally smooth over R_p; with formal unramifiedness it is formally étale over R_p, hence over R. The presentation of S_q as a localization of the finitely presented R_p-algebra S_p is set up as in Mathlib's proof of Algebra.IsSmoothAt.of_formallySmooth_fiber.

Main results

• Algebra.isEtaleAt_iff_flat_and_isUnramifiedAt: for S finitely presented over R, S is étale over R at q iff S_q is flat over R and S is unramified over R at q.
• Algebra.IsEtaleAt.flat_localization: the flatness half of the forward direction.
• Algebra.IsEtaleAt.of_flat_of_isUnramifiedAt: the reverse direction, the pointwise form of Mathlib's Algebra.IsEtaleAt.of_isUnramifiedAt_of_flat.
• Algebra.IsEtaleAt.of_isUnramifiedAt_of_isDedekindDomain: if R_p is a Dedekind domain, for instance a discrete valuation ring, and S_q is a domain but not a field, then flatness is automatic, so S is étale over R at q as soon as it is unramified there. This is the case of dimension one of purity of the branch locus.

References

• The Stacks Project, Lemma 10.151.8 (08WD), the global form: étale is flat, unramified and of finite presentation.
• The Stacks Project, Tag 00TF, smoothness at a prime from flatness and a smooth fibre.
• The Stacks Project, Lemma 58.21.4 (0BMB), purity of the branch locus, whose proof starts from the case of dimension one.

theorem Algebra.IsEtaleAt.flat_localization {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime] [IsEtaleAt R q] : Module.Flat R (Localization.AtPrime q)

If S is finitely presented over R and étale at a prime q, then S_q is flat over R.

theorem Algebra.IsEtaleAt.of_flat_of_isUnramifiedAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime] [Module.Flat R (Localization.AtPrime q)] [IsUnramifiedAt R q] : IsEtaleAt R q

If S is finitely presented over R, unramified at a prime q, and S_q is flat over R, then S is étale over R at q.

theorem Algebra.isEtaleAt_iff_flat_and_isUnramifiedAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime] : IsEtaleAt R q ↔ Module.Flat R (Localization.AtPrime q) ∧ IsUnramifiedAt R q

A finitely presented R-algebra S is étale over R at a prime q if and only if S_q is flat over R and S is unramified over R at q.

theorem Algebra.IsEtaleAt.of_isUnramifiedAt_of_isDedekindDomain {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime] [IsDedekindDomain (Localization.AtPrime (Ideal.under R q))] [IsDomain (Localization.AtPrime q)] (hq : ¬IsField (Localization.AtPrime q)) [IsUnramifiedAt R q] : IsEtaleAt R q

Purity in dimension one. Let S be finitely presented over R, and q a prime of S over p such that R_p is a Dedekind domain, for instance a discrete valuation ring, and S_q is a domain but not a field. If S is unramified over R at q, then it is étale over R at q.