Henselian pairs under directed colimits

Let (G i, I i) be a directed system of pairs of a commutative ring and an ideal, indexed by a nonempty directed preorder, whose transition maps f i j carry I i into I j. The main result, Ring.DirectLimit.henselianRing, is that if every (G i, I i) is Henselian, then Ring.DirectLimit G f is Henselian along the colimit ideal ⨆ i, (I i).map (of G f i).

A monic polynomial over the colimit with a simple root modulo the colimit ideal comes, together with its approximate root and the witnesses for both conditions, from a single stage (using the descent lemmas of TauCeti.Algebra.Colimit.Ring); the root found there maps to the required root in the colimit. This is the filtered-colimit case of the permanence properties of Henselian pairs. Directedness is essential: the coproduct of two copies of (ℤ_[p], (p)), which is not a directed colimit, is not Henselian along p.

Main results

• Ring.DirectLimit.henselianRing: a directed colimit of Henselian pairs is Henselian along the colimit ideal.

References

• Stacks Project, Lemma 15.11.13.
• Stacks Project, Example 15.11.14 for the failure along non-filtered colimits.

theorem Ring.DirectLimit.henselianRing {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {I : (i : ι) → Ideal (G i)} [Nonempty ι] [IsDirectedOrder ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [∀ (i : ι), HenselianRing (G i) (I i)] (hI : ∀ (i j : ι) (hij : i ≤ j), I i ≤ Ideal.comap (f i j hij) (I j)) : HenselianRing (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) (⨆ (i : ι), Ideal.map (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) (I i))

Henselian pairs are stable under directed colimits. If every (G i, I i) is a Henselian pair and the transition maps carry I i into I j, then the directed colimit Ring.DirectLimit G f is Henselian along the colimit ideal ⨆ i, (I i).map (of G f i).