The Jacobson radical of the henselization

The ideal extended to the henselization lies in its Jacobson radical. The key fact is that an element of an étale neighbourhood which is invertible modulo the extended ideal becomes invertible in the henselization: localizing that neighbourhood at the element is another neighbourhood. This supplies the radical condition in the definition of a henselian pair, without assuming that the original ideal lies in the Jacobson radical.

As a consequence, the henselization is the zero ring exactly when the ideal is the unit ideal: along ⊤ the extended ideal is everything, and otherwise the henselization keeps the nonzero quotient R ⧸ I.

References

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

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

An element of a neighbourhood which is a unit modulo the extended ideal becomes a unit in the henselization.

theorem TauCeti.Henselization.extended_le_jacobson {R : Type u} [CommRing R] (I : Ideal R) : extended I ≤ ⊥.jacobson

The extension of the original ideal to its henselization is contained in the Jacobson radical, with no assumption on the original ideal.

theorem TauCeti.Henselization.subsingleton_iff {R : Type u} [CommRing R] (I : Ideal R) : Subsingleton ↑(algebra I) ↔ I = ⊤

The henselization of (R, I) is the zero ring exactly when I is the unit ideal.

theorem TauCeti.Henselization.nontrivial_iff {R : Type u} [CommRing R] (I : Ideal R) : Nontrivial ↑(algebra I) ↔ I ≠ ⊤

The henselization of (R, I) is a nonzero ring exactly when I is a proper ideal.