The henselization of a pair is henselian

For a ring R and an ideal I, the henselization algebra I, the filtered colimit of the étale neighbourhoods of (R, I), is henselian along the extended ideal extended I.

The proof descends a monic polynomial with a simple root modulo the extended ideal to a single étale neighbourhood B. Every stage B has the same closed fibre as the henselization, so the simple-root hypotheses hold modulo I B. Adjoining a root of the polynomial to B and inverting its derivative and the cofactor of the root gives a standard étale B-algebra. Its closed fibre is still R ⧸ I, so it is a further neighbourhood, and it contains an actual root.

Main results

• TauCeti.Henselization.quotientMap_stage_bijective: each stage map induces an isomorphism of closed fibres.
• TauCeti.Henselization.exists_hom_isRoot_sub_mem: a simple root modulo I at an étale neighbourhood becomes a root at a further étale neighbourhood.
• TauCeti.Henselization.henselian: the pair (algebra I, extended I) is henselian.

References

• Stacks Project, Tag 0A02, the henselization of a pair is a henselian pair.

theorem TauCeti.Henselization.map_le_comap_stage_extended {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) : Ideal.map (algebraMap R ↑B.obj) I ≤ Ideal.comap (↑(stage I B)) (extended I)

The stage map of an étale neighbourhood carries its extended ideal into the extended ideal of the henselization.

theorem TauCeti.Henselization.quotientMap_stage_bijective {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) : Function.Bijective ⇑(Ideal.quotientMap (extended I) ↑(stage I B) ⋯)

Every étale neighbourhood has the same closed fibre as the henselization: its stage map induces an isomorphism modulo the extended ideals.

theorem TauCeti.Henselization.comap_stage_extended {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) : Ideal.comap (↑(stage I B)) (extended I) = Ideal.map (algebraMap R ↑B.obj) I

An element of an étale neighbourhood lies in its extended ideal exactly when its image in the henselization lies in the extended ideal.

theorem TauCeti.Henselization.isUnit_quotient_stage_iff {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) (b : ↑B.obj) : IsUnit ((Ideal.Quotient.mk (extended I)) ((stage I B) b)) ↔ IsUnit ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↑B.obj) I)) b)

An element of an étale neighbourhood is a unit modulo its extended ideal exactly when its image in the henselization is a unit modulo the extended ideal.

theorem TauCeti.Henselization.exists_hom_isRoot_sub_mem {R : Type u} [CommRing R] (I : Ideal R) (B : Neighbourhood I) {p : Polynomial ↑B.obj} (hp : p.Monic) {a : ↑B.obj} (hpa : Polynomial.eval a p ∈ Ideal.map (algebraMap R ↑B.obj) I) (hu : IsUnit ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↑B.obj) I)) (Polynomial.eval a (Polynomial.derivative p)))) : ∃ (C : Neighbourhood I) (f : B ⟶ C) (c : ↑C.obj), (Polynomial.map (↑(CommAlgCat.Hom.hom f.hom)) p).IsRoot c ∧ c - (CommAlgCat.Hom.hom f.hom) a ∈ Ideal.map (algebraMap R ↑C.obj) I

A simple root modulo the extended ideal at an étale neighbourhood becomes an actual root at a further étale neighbourhood, congruent to it modulo the extended ideal.

instance TauCeti.Henselization.henselian {R : Type u} [CommRing R] (I : Ideal R) : HenselianRing (↑(algebra I)) (extended I)

The henselization of a pair is henselian. The pair formed by the henselization of (R, I) and the extended ideal is a henselian pair, with no hypothesis on R or I.