Sections of étale algebras over a Henselian local ring

Let R be a Henselian local ring with residue field k, and let S be an étale R-algebra. Reducing modulo the maximal ideal is a bijection from R-algebra maps S → R to R-algebra maps S → k (TauCeti.HenselianLocalRing.comp_bijective): every k-point of S lifts uniquely to an R-point. This is one of the equivalent characterisations of Henselian local rings, and the analogue for the maximal ideal of Algebra.FormallyEtale.comp_bijective, where the ideal is square-zero.

For a standard étale algebra R[X]_g ⧸ (f) an R-point is a root a of f with g(a) a unit, so this is Hensel's lemma: f'(a) is a unit at such a root. A general étale algebra is standard étale after inverting an element g outside the kernel of a given k-point (Algebra.IsEtaleAt.exists_isStandardEtale), and both k-points and their lifts extend uniquely to the localisation.

Consequently a strictly Henselian local ring, one whose residue field is separably closed, has no nonsplit finite étale covers (TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing): a faithfully flat finite étale algebra has a k-point because k is separably closed, and this lifts to a section. Such rings need be neither fields nor reduced. As the spectrum of a local ring is connected, every finite étale algebra over a strictly Henselian local ring is moreover a finite product of copies of the base (Algebra.IsFiniteSplit.of_henselianLocalRing).

Main results

• TauCeti.HenselianLocalRing.comp_bijective: over a Henselian local ring, R-points of an étale algebra are in bijection with its points over the residue field.
• TauCeti.HenselianLocalRing.comp_bijective_of_algebra: the same for an étale algebra over an arbitrary base R and a Henselian local R-algebra S.
• TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing: a Henselian local ring with separably closed residue field has no nonsplit finite étale covers.
• Algebra.IsFiniteSplit.of_henselianLocalRing: over such a ring every finite étale algebra is a finite product of copies of the base.

References

• Stacks Project, Tag 04GG, characterisations of Henselian local rings by sections of étale algebras.
• Stacks Project, Lemma 10.153.11, Tag 08HQ, unique lifting of residue field points of an étale algebra to a Henselian local algebra over an arbitrary base.
• P. Scholze, Étale cohomology of diamonds, Lemma 15.3, for rings without nonsplit finite étale covers.

theorem TauCeti.HenselianLocalRing.comp_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [HenselianLocalRing R] [CommRing S] [Algebra R S] [Algebra.Etale R S] : Function.Bijective (Algebra.ofId R (IsLocalRing.ResidueField R)).comp

Over a Henselian local ring R, reduction modulo the maximal ideal is a bijection from the R-points of an étale R-algebra S to its points over the residue field: every R-algebra map S → k lifts uniquely to an R-algebra map S → R. Compare Algebra.FormallyEtale.comp_bijective, the same statement for square-zero ideals over an arbitrary base.

theorem TauCeti.HenselianLocalRing.comp_bijective_of_algebra {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [HenselianLocalRing S] [Algebra R S] [CommRing A] [Algebra R A] [Algebra.Etale R A] : Function.Bijective (IsScalarTower.toAlgHom R S (IsLocalRing.ResidueField S)).comp

The relative form of comp_bijective: for a Henselian local R-algebra S and an étale R-algebra A, reduction modulo the maximal ideal of S is a bijection from R-algebra maps A → S to R-algebra maps A → κ(S). The base is arbitrary; comp_bijective is the case S = R.

instance TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing (R : Type u) [CommRing R] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] : IsFiniteEtaleSplit R

A Henselian local ring with separably closed residue field, that is, a strictly Henselian local ring, has no nonsplit finite étale covers: a faithfully flat finite étale algebra has a point over the separably closed residue field, which lifts to a section.

theorem Algebra.IsFiniteSplit.of_henselianLocalRing (R : Type u) [CommRing R] [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] (T : Type u_1) [CommRing T] [Algebra R T] [Etale R T] [Module.Finite R T] : IsFiniteSplit R T

Finite étale algebras over a strictly Henselian local ring split: over a Henselian local ring R with separably closed residue field, every finite étale R-algebra is R-isomorphic to a finite product Fin n → R of copies of R.