Henselian rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

henselian_ring: a typeclass on commutative rings, asserting that the ring is Henselian at the ideal I.
henselian_local_ring: 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
is_adic_complete.henselian: 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 os 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

source

theorem is_local_ring_hom_of_le_jacobson_bot {R : Type u_1} [comm_ring R] (I : ideal R) (h : I ≤ ⊥.jacobson) :

is_local_ring_hom (ideal.quotient.mk I)

source

@[class]

structure henselian_ring (R : Type u_1) [comm_ring R] (I : ideal R) :

Prop

jac : I ≤ ⊥.jacobson
is_henselian : ∀ (f : polynomial R), f.monic → ∀ (a₀ : R), polynomial.eval a₀ f ∈ I → is_unit (⇑(ideal.quotient.mk I) (polynomial.eval a₀ (⇑polynomial.derivative f))) → (∃ (a : R), f.is_root a ∧ a - a₀ ∈ I)

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.

Instances of this typeclass

source

@[class]

structure henselian_local_ring (R : Type u_1) [comm_ring R] :

Prop

to_local_ring : local_ring R
is_henselian : ∀ (f : polynomial R), f.monic → ∀ (a₀ : R), polynomial.eval a₀ f ∈ local_ring.maximal_ideal R → is_unit (polynomial.eval a₀ (⇑polynomial.derivative f)) → (∃ (a : R), f.is_root a ∧ a - a₀ ∈ local_ring.maximal_ideal R)

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 henselian_ring.

Instances of this typeclass

field.henselian

source

@[protected, instance]

def field.henselian (K : Type u_1) [field K] :

henselian_local_ring K

source

theorem henselian_local_ring.tfae (R : Type u) [comm_ring R] [local_ring R] :

[henselian_local_ring R, ∀ (f : polynomial R), f.monic → ∀ (a₀ : local_ring.residue_field R), ⇑(polynomial.aeval a₀) f = 0 → ⇑(polynomial.aeval a₀) (⇑polynomial.derivative f) ≠ 0 → (∃ (a : R), f.is_root a ∧ ⇑(local_ring.residue R) a = a₀), ∀ {K : Type u} [_inst_3 : 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.is_root a ∧ ⇑φ a = a₀)].tfae

source

@[protected, instance]

def local_ring.maximal_ideal.henselian_ring (R : Type u_1) [comm_ring R] [hR : henselian_local_ring R] :

henselian_ring R (local_ring.maximal_ideal R)

source

@[protected, instance]

def is_adic_complete.henselian_ring (R : Type u_1) [comm_ring R] (I : ideal R) [is_adic_complete I R] :

henselian_ring R I

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