Sections of étale neighbourhoods of a Henselian pair

Let (S, J) be a Henselian pair. An étale neighbourhood of (S, J) is an étale S-algebra C with S ⧸ J ≅ C ⧸ JC, so that C has exactly one S-algebra map to S ⧸ J. This file shows that C has exactly one S-algebra map to S. These sections are the maps out of the stages of the henselization of a pair into a Henselian pair. Existence holds more generally for flat, finitely presented, quasi-finite algebras C with S ⧸ J ≅ C ⧸ JC.

Implementation notes

By the global form of Zariski's main theorem, C agrees with a module-finite subalgebra C' on finitely many basic opens covering Spec C. These produce an element of C' that is idempotent modulo JC' and cuts out a summand of C' ⧸ JC' generated by one element over S ⧸ J. It lifts to an idempotent e of C' (TauCeti.HenselianRing.exists_isIdempotentElem_sub_mem_map), and Nakayama's lemma gives e C = S e. Flatness then makes S → C ⧸ (1 - e) an isomorphism.

Main results

• TauCeti.Henselization.nonempty_algHom_of_bijective_reducedMap: a flat, finitely presented, quasi-finite S-algebra C with S ⧸ J ≅ C ⧸ JC has an S-algebra map to S.
• TauCeti.Henselization.nonempty_unique_algHom_of_isNeighbourhood: an étale neighbourhood of a Henselian pair has exactly one S-algebra map to S.
• TauCeti.Henselization.IsNeighbourhood.nonempty_algHom: an étale neighbourhood of (R, I) has an R-algebra map to every Henselian pair (S, J) with IS ⊆ J.

References

• Stacks Project, Lemma 15.11.6, condition (2).
• Stacks Project, Tag 00Q9, Zariski's main theorem.

theorem TauCeti.Henselization.nonempty_algHom_of_bijective_reducedMap {S : Type u} [CommRing S] (J : Ideal S) {C : Type v} [CommRing C] [Algebra S C] [HenselianRing S J] [Algebra.FinitePresentation S C] [Module.Flat S C] [Algebra.QuasiFinite S C] (hC : Function.Bijective ⇑(reducedMap J C)) : Nonempty (C →ₐ[S] S)

Sections over a Henselian pair. Let (S, J) be a Henselian pair and let C be a flat, finitely presented, quasi-finite S-algebra such that S ⧸ J → C ⧸ JC is bijective. Then there is an S-algebra map C → S.

theorem TauCeti.Henselization.nonempty_unique_algHom_of_isNeighbourhood {S : Type u} [CommRing S] (J : Ideal S) [HenselianRing S J] {C : CommAlgCat S} (hC : IsNeighbourhood J C) : Nonempty (Unique (↑C →ₐ[S] S))

Étale neighbourhoods of a Henselian pair have unique sections. If (S, J) is a Henselian pair and C is an étale neighbourhood of (S, J), there is exactly one S-algebra map C → S.

theorem TauCeti.Henselization.IsNeighbourhood.nonempty_algHom {R : Type u_1} [CommRing R] {I : Ideal R} {B : CommAlgCat R} (hB : IsNeighbourhood I B) {S : Type u_2} [CommRing S] [Algebra R S] {J : Ideal S} [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) : Nonempty (↑B →ₐ[R] S)

An étale neighbourhood of (R, I) has an R-algebra map to every henselian pair (S, J) receiving a map of pairs from (R, I): the base change S ⊗[R] B is an étale neighbourhood of (S, J), and so has a section.