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 ofR
- for every polynomial
f
overR
, with a simple roota₀
over the quotient ringR/I
, there exists a lifta : R
ofa₀
that is a root off
.
(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 idealI
.HenselianLocalRing
: a typeclass on commutative rings, asserting that the ring is local Henselian.Field.henselian
: fields are Henselian local ringsHenselian.TFAE
: equivalent ways of expressing the Henselian property for local ringsIsAdicComplete.henselianRing
: a ringR
with idealI
that isI
-adically complete is Henselian atI
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
Alias of isLocalHom_of_le_jacobson_bot
.
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ℤ
.)
- 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
Instances
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
.
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A ring R
that is I
-adically complete is Henselian at I
.
Equations
- ⋯ = ⋯