Henselian rings

This file gathers the basic consequences of Henselianity that Mathlib does not provide.

Mathlib has both halves of the comparison between HenselianRing R I, which lifts a simple root over R ⧸ I, and HenselianLocalRing R, which lifts a simple root over the residue field, except for the step that produces the local class from the ideal-theoretic one at I = 𝔪. So IsAdicComplete.henselianRing never reaches HenselianLocalRing, and the Henselian API is unavailable for a complete local ring such as the integers of a complete discretely valued field.

The step is short: the two differ only in their simplicity hypothesis, IsUnit (f' a₀) against IsUnit (Ideal.Quotient.mk 𝔪 (f' a₀)), and over a local ring a unit maps to a unit.

The second half of the file extracts roots. Let R be a ring that is Henselian at an ideal J, and let n be a natural number that is invertible in R. Then every element w congruent to 1 modulo an ideal I ≤ J has an n-th root that is itself congruent to 1 modulo I.

This is the standard source of n-th roots of principal units away from the residue characteristic: over the integer ring of a local field it shows that each positive-depth step of the unit filtration is carried onto itself by the n-th power map.

Without assuming 2 invertible, every element of 1 + 4J is a square. This supplies deep square roots in residue characteristic two, by solving t² + t = c for c ∈ J.

Main results

• TauCeti.HenselianRing.henselianLocalRing: a local ring that is Henselian at its maximal ideal is a Henselian local ring.
• TauCeti.IsAdicComplete.henselianLocalRing: a local ring that is complete for the adic topology of its maximal ideal is a Henselian local ring.
• TauCeti.HenselianLocalRing.exists_pow_eq_of_residue_pow_eq: a simple power root in the residue field lifts to a root with the same residue.
• TauCeti.HenselianRing.exists_pow_eq_and_sub_one_mem_of_sub_one_mem: if n is invertible, I ≤ J and w ≡ 1 mod I, then w = a ^ n for some a ≡ 1 mod I.

Implementation notes

Hensel's lemma applied to X ^ n - w at the approximate root 1 produces a root a with a ≡ 1 modulo J only. The congruence is then sharpened to I through the factorization a ^ n - 1 = (1 + a + ⋯ + a ^ (n - 1)) * (a - 1), whose first factor reduces to n modulo J and is therefore a unit, J lying in the Jacobson radical.

theorem TauCeti.HenselianRing.henselianLocalRing (R : Type u_1) [CommRing R] [IsLocalRing R] [HenselianRing R (IsLocalRing.maximalIdeal R)] : HenselianLocalRing R

A local ring that is Henselian at its maximal ideal is a Henselian local ring. The two hypotheses differ only in their simplicity condition, which asks the derivative to be a unit in the residue field rather than in the ring, and over a local ring the image of a unit is a unit.

This is not an instance: Mathlib already registers the converse implication as one, so the pair would form an instance cycle.

instance TauCeti.IsAdicComplete.henselianLocalRing (R : Type u_1) [CommRing R] [IsLocalRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] : HenselianLocalRing R

A local ring that is complete for the adic topology of its maximal ideal is a Henselian local ring. This is Mathlib's IsAdicComplete.henselianRing at I = 𝔪, read through TauCeti.HenselianRing.henselianLocalRing.

theorem TauCeti.HenselianLocalRing.exists_pow_eq_of_residue_pow_eq {R : Type u_1} [CommRing R] [HenselianLocalRing R] {n : ℕ} (hn : IsUnit ↑n) {x₀ u : R} (hx₀ : IsUnit x₀) (h : (IsLocalRing.residue R) x₀ ^ n = (IsLocalRing.residue R) u) : ∃ (x : R), x ^ n = u ∧ (IsLocalRing.residue R) x = (IsLocalRing.residue R) x₀

If n is a unit, a unit residue root of X ^ n - u lifts to a root with the same residue.

theorem TauCeti.HenselianRing.exists_pow_eq_and_sub_one_mem_of_sub_one_mem {R : Type u_1} [CommRing R] {I J : Ideal R} [HenselianRing R J] (hI : I ≤ J) {n : ℕ} (hn : IsUnit ↑n) {w : R} (hw : w - 1 ∈ I) : ∃ (a : R), a ^ n = w ∧ a - 1 ∈ I

In a ring Henselian at an ideal J, if n is invertible then every element congruent to 1 modulo an ideal I ≤ J is the n-th power of an element congruent to 1 modulo I.

theorem TauCeti.HenselianRing.exists_sq_add_eq_of_mem {R : Type u_1} [CommRing R] {J : Ideal R} [HenselianRing R J] {c : R} (hc : c ∈ J) : ∃ t ∈ J, t ^ 2 + t = c

In a ring Henselian at J, an element c ∈ J has the form t² + t for some t ∈ J. This is the simple-root form of Hensel's lemma that also works in residue characteristic two.

theorem TauCeti.HenselianRing.isSquare_one_add_four_mul_of_mem {R : Type u_1} [CommRing R] {J : Ideal R} [HenselianRing R J] {c : R} (hc : c ∈ J) : IsSquare (1 + 4 * c)

In a ring Henselian at J, every element of 1 + 4J is a square. No invertibility assumption on 2 in the ring or its residue rings is needed.