Henselian rings

In this file we set up the basic theory of Henselian (local) rings. A ring R is Henselian at an ideal I if the following conditions hold:

• I is contained in the Jacobson radical of R
• for every polynomial f over R, with a simple root a₀ over the quotient ring R/I, there exists a lift a : R of a₀ that is a root of f.

(Here, saying that a root b of a polynomial g is simple means that g.derivative.eval b is a unit. Warning: if R/I is not a field then it is not enough to assume that g has a factorization into monic linear factors in which X - b shows up only once; for example 1 is not a simple root of X^2-1 over ℤ/4ℤ.)

A local ring R is Henselian if it is Henselian at its maximal ideal. In this case the first condition is automatic, and in the second condition we may ask for f.derivative.eval a ≠ 0, since the quotient ring R/I is a field in this case.

Main declarations

• HenselianRing: a typeclass on commutative rings, asserting that the ring is Henselian at the ideal I.
• HenselianLocalRing: a typeclass on commutative rings, asserting that the ring is local Henselian.
• Field.henselian: fields are Henselian local rings
• Henselian.TFAE: equivalent ways of expressing the Henselian property for local rings
• IsAdicComplete.henselianRing: a ring R with ideal I that is I-adically complete is Henselian at I

References

https://stacks.math.columbia.edu/tag/04GE

TODO

After a good API for etale ring homomorphisms has been developed, we can give more equivalent characterization of Henselian rings.

In particular, this can give a proof that factorizations into coprime polynomials can be lifted from the residue field to the Henselian ring.

The following gist contains some code sketches in that direction. https://gist.github.com/jcommelin/47d94e4af092641017a97f7f02bf9598

theorem isLocalHom_of_le_jacobson_bot {R : Type u_1} [CommRing R] (I : Ideal R) (h : I ≤ ⊥.jacobson) : IsLocalHom (Ideal.Quotient.mk I)

@[deprecated isLocalHom_of_le_jacobson_bot]

theorem isLocalRingHom_of_le_jacobson_bot {R : Type u_1} [CommRing R] (I : Ideal R) (h : I ≤ ⊥.jacobson) : IsLocalHom (Ideal.Quotient.mk I)

Alias of isLocalHom_of_le_jacobson_bot.

class HenselianRing (R : Type u_1) [CommRing R] (I : Ideal R) : Prop

A ring R is Henselian at an ideal I if the following condition holds: for every polynomial f over R, with a simple root a₀ over the quotient ring R/I, there exists a lift a : R of a₀ that is a root of f.

(Here, saying that a root b of a polynomial g is simple means that g.derivative.eval b is a unit. Warning: if R/I is not a field then it is not enough to assume that g has a factorization into monic linear factors in which X - b shows up only once; for example 1 is not a simple root of X^2-1 over ℤ/4ℤ.)

• jac : I ≤ ⊥.jacobson
• is_henselian : ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ I → IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I

theorem HenselianRing.jac {R : Type u_1} : ∀ {inst : CommRing R} {I : Ideal R} [self : HenselianRing R I], I ≤ ⊥.jacobson

theorem HenselianRing.is_henselian {R : Type u_1} : ∀ {inst : CommRing R} {I : Ideal R} [self : HenselianRing R I] (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ I → IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I

class HenselianLocalRing (R : Type u_1) [CommRing R] extends LocalRing : Prop

A local ring R is Henselian if the following condition holds: for every polynomial f over R, with a simple root a₀ over the residue field, there exists a lift a : R of a₀ that is a root of f. (Recall that a root b of a polynomial g is simple if it is not a double root, so if g.derivative.eval b ≠ 0.)

In other words, R is local Henselian if it is Henselian at the ideal I, in the sense of HenselianRing.

• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b
• is_henselian : ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ LocalRing.maximalIdeal R → IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ LocalRing.maximalIdeal R

theorem HenselianLocalRing.is_henselian {R : Type u_1} : ∀ {inst : CommRing R} [self : HenselianLocalRing R] (f : Polynomial R), f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ LocalRing.maximalIdeal R → IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ LocalRing.maximalIdeal R

@[instance 100]

instance Field.henselian (K : Type u_1) [Field K] : HenselianLocalRing K

Equations

• ⋯ = ⋯

theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [LocalRing R] : [HenselianLocalRing R, ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : LocalRing.ResidueField R), (Polynomial.aeval a₀) f = 0 → (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ (a : R), f.IsRoot a ∧ (LocalRing.residue R) a = a₀, ∀ {K : Type u} [inst : Field K] (φ : R →+* K), Function.Surjective ⇑φ → ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : K), Polynomial.eval₂ φ a₀ f = 0 → Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ (a : R), f.IsRoot a ∧ φ a = a₀].TFAE

instance instHenselianRingMaximalIdeal (R : Type u_1) [CommRing R] [hR : HenselianLocalRing R] : HenselianRing R (LocalRing.maximalIdeal R)

Equations

• ⋯ = ⋯

@[instance 100]

instance IsAdicComplete.henselianRing (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] : HenselianRing R I

A ring R that is I-adically complete is Henselian at I.

Equations

• ⋯ = ⋯