The universal property of the henselization of a pair

The henselization of (R, I) is universal among henselian pairs (S, J) receiving a map of pairs from (R, I): there is exactly one R-algebra map from the henselization to S, and it carries the extended ideal into J. In particular a henselian pair is its own henselization.

Uniqueness holds under the weaker hypothesis that I generates an ideal of S inside its Jacobson radical: an R-algebra map out of the henselization is determined by its restrictions to the étale neighbourhoods, and each restriction is a map out of an étale algebra which is already determined modulo IS. For existence, each étale neighbourhood B of (R, I) base changes to an étale neighbourhood S ⊗[R] B of (S, J), which has a section over the henselian pair (S, J). By uniqueness these maps B → S form a cocone, and the colimit property of the henselization assembles them.

Main results

• TauCeti.Henselization.algHom_ext_of_map_le_jacobson: maps out of the henselization are unique once IS lies in the Jacobson radical of S.
• TauCeti.Henselization.ringHom_ext_of_map_le_jacobson: ring maps out of the henselization of (R, I) agreeing on R are equal once the image of I lies in the Jacobson radical.
• TauCeti.Henselization.lift: the map from the henselization of (R, I) to a henselian pair (S, J) with IS ⊆ J.
• TauCeti.Henselization.existsUnique_lift: the universal property of the henselization.
• TauCeti.Henselization.algEquivOfHenselianRing: if (R, I) is henselian, its henselization is R.

Implementation notes

The henselization is a colimit in CommAlgCat.{u} R, while the target S may live in any universe. The compatible maps B → S are assembled by the shared construction SmallFilteredAlgebraColimit.descOfCompatible, which goes through a u-small subalgebra of S.

References

• Stacks Project, Lemma 15.12.1, the universal property of the henselization of a pair.
• The Stacks Project, Lemma 15.11.5, uniqueness of sections modulo an ideal in the Jacobson radical.

theorem TauCeti.Henselization.algHom_ext_of_map_le_jacobson {R : Type u} [CommRing R] {I : Ideal R} {S : Type u_1} [CommRing S] [Algebra R S] (hI : Ideal.map (algebraMap R S) I ≤ ⊥.jacobson) {f g : ↑(algebra I) →ₐ[R] S} : f = g

Two R-algebra maps out of the henselization of (R, I) agree as soon as I generates an ideal of the target inside its Jacobson radical. In particular, maps of pairs from the henselization of (R, I) to a henselian pair are unique.

theorem TauCeti.Henselization.ringHom_ext_of_map_le_jacobson {R : Type u} [CommRing R] {I : Ideal R} {T : Type u_1} [CommRing T] {g₁ g₂ : ↑(algebra I) →+* T} (h : g₁.comp (algebraMap R ↑(algebra I)) = g₂.comp (algebraMap R ↑(algebra I))) (hI : Ideal.map (g₁.comp (algebraMap R ↑(algebra I))) I ≤ ⊥.jacobson) : g₁ = g₂

Two ring maps out of the henselization of (R, I) which agree on R are equal as soon as I generates an ideal of the target inside its Jacobson radical.

noncomputable def TauCeti.Henselization.lift {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] [Algebra R S] {J : Ideal S} [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) : ↑(algebra I) →ₐ[R] S

The R-algebra map from the henselization of (R, I) to a henselian pair (S, J) with IS ⊆ J. It is the unique R-algebra map (existsUnique_lift).

theorem TauCeti.Henselization.eq_lift {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] [Algebra R S] {J : Ideal S} [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) (f : ↑(algebra I) →ₐ[R] S) : f = lift hIJ

Every R-algebra map from the henselization of (R, I) to a henselian pair (S, J) with IS ⊆ J is lift.

theorem TauCeti.Henselization.lift_comp_stage {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] [Algebra R S] {J : Ideal S} [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) (B : Neighbourhood I) (φ : ↑B.obj →ₐ[R] S) : (lift hIJ).comp (stage I B) = φ

On the stage of an étale neighbourhood B, lift restricts to any R-algebra map B → S: there is exactly one such map.

theorem TauCeti.Henselization.lift_stage {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] [Algebra R S] {J : Ideal S} [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) (B : Neighbourhood I) (φ : ↑B.obj →ₐ[R] S) (b : ↑B.obj) : (lift hIJ) ((stage I B) b) = φ b

On the stage of an étale neighbourhood B, lift agrees with any R-algebra map B → S.

theorem TauCeti.Henselization.existsUnique_lift {R : Type u} [CommRing R] {I : Ideal R} {S : Type v} [CommRing S] [Algebra R S] (J : Ideal S) [HenselianRing S J] (hIJ : Ideal.map (algebraMap R S) I ≤ J) : ∃! f : ↑(algebra I) →ₐ[R] S, Ideal.map f (extended I) ≤ J

The universal property of the henselization. For a henselian pair (S, J) receiving a map of pairs from (R, I), there is a unique R-algebra map from the henselization of (R, I) to S carrying the extended ideal into J.

noncomputable def TauCeti.Henselization.algEquivOfHenselianRing {R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I] : ↑(algebra I) ≃ₐ[R] R

A henselian pair is its own henselization: if (R, I) is henselian, the structure map from R to its henselization along I is an isomorphism.

@[simp]

theorem TauCeti.Henselization.algEquivOfHenselianRing_symm_apply {R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I] (r : R) : (algEquivOfHenselianRing I).symm r = (algebraMap R ↑(algebra I)) r

The inverse of algEquivOfHenselianRing is the structure map of the henselization.

theorem TauCeti.Henselization.bijective_algebraMap_of_henselianRing {R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I] : Function.Bijective ⇑(algebraMap R ↑(algebra I))

If (R, I) is henselian, the structure map from R to its henselization along I is bijective.