The henselization of a local ring

The henselization of a pair (R, 𝔪) with 𝔪 a maximal ideal is a henselian local ring whose maximal ideal is the extended ideal 𝔪 R^h. When R is local with maximal ideal 𝔪, the structure map R → R^h is a local homomorphism inducing an isomorphism of residue fields, and R^h is universal among local homomorphisms from R to henselian local rings. So the henselization of the pair (R, 𝔪) is the henselization of the local ring R.

Main results

• TauCeti.Henselization.henselianLocalRing: the henselization along a maximal ideal is a henselian local ring, with maximal ideal extended I (maximalIdeal_eq_extended).
• TauCeti.Henselization.isLocalHom_algebraMap: for a local ring R, the structure map to the henselization along the maximal ideal is local.
• TauCeti.Henselization.residueField_map_bijective: it induces an isomorphism of residue fields.
• TauCeti.Henselization.existsUnique_isLocalHom: every local homomorphism from R to a henselian local ring factors through a unique local homomorphism out of the henselization.

References

• Stacks Project, Lemma 15.12.3, the henselization of the pair (R, 𝔪) is the henselization of the local ring R.
• Stacks Project, Definition 10.155.3, the henselization of a local ring.

instance TauCeti.Henselization.isLocalRing {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] : IsLocalRing ↑(algebra I)

The henselization along a maximal ideal is a local ring.

theorem TauCeti.Henselization.maximalIdeal_eq_extended {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] : IsLocalRing.maximalIdeal ↑(algebra I) = extended I

The maximal ideal of the henselization along a maximal ideal I is the extended ideal.

instance TauCeti.Henselization.henselianLocalRing {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] : HenselianLocalRing ↑(algebra I)

The henselization along a maximal ideal is a henselian local ring.

theorem TauCeti.Henselization.isLocalHom_lift {R : Type u} [CommRing R] (I : Ideal R) [I.IsMaximal] {S : Type v} [CommRing S] [HenselianLocalRing S] [Algebra R S] (hI : Ideal.map (algebraMap R S) I ≤ IsLocalRing.maximalIdeal S) : IsLocalHom (lift hI)

The map from the henselization along a maximal ideal I to a henselian local ring in which I generates a proper ideal is a local homomorphism.

instance TauCeti.Henselization.isLocalHom_algebraMap (R : Type u) [CommRing R] [IsLocalRing R] : IsLocalHom (algebraMap R ↑(algebra (IsLocalRing.maximalIdeal R)))

The structure map from a local ring to its henselization along the maximal ideal is a local homomorphism.

theorem TauCeti.Henselization.residueField_map_bijective (R : Type u) [CommRing R] [IsLocalRing R] : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R ↑(algebra (IsLocalRing.maximalIdeal R))))

The structure map from a local ring to its henselization along the maximal ideal induces an isomorphism of residue fields.

theorem TauCeti.Henselization.existsUnique_isLocalHom {R : Type u} [CommRing R] [IsLocalRing R] {S : Type v} [CommRing S] [HenselianLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] : ∃! f : ↑(algebra (IsLocalRing.maximalIdeal R)) →ₐ[R] S, IsLocalHom f

The universal property of the henselization of a local ring. Every local homomorphism from a local ring R to a henselian local ring S factors through a unique local R-algebra map from the henselization of R along its maximal ideal. Every R-algebra map from the henselization to S is in fact local and equal to this one (eq_lift).