Hensel's lemma with an estimate over a discrete valuation ring #
Let A be a discrete valuation ring with additive valuation v = IsDiscreteValuationRing.addVal,
and let F be a polynomial over A. If y₀ is an approximate root of F in the sense that
2 v(F'(y₀)) < v(F(y₀)), then F has a root z with
v(F(y₀)) = v(F'(y₀)) + v(z − y₀), and z is the only root of F with
v(F'(y₀)) < v(z − y₀). This is Mathlib's hensels_lemma, which is stated over ℤ_[p] in norm
spelling, here over an arbitrary Henselian discrete valuation ring (for instance a complete one,
by TauCeti.IsAdicComplete.henselianLocalRing) in addVal spelling.
The quantitative statement is what distinguishes this from HenselianLocalRing, which lifts a
simple root modulo the maximal ideal without a distance bound: the estimate locates the root in a
ball around y₀ whose radius is read off F(y₀) and F'(y₀), which is what is needed to count
roots of nearby polynomials. If U f + V f' = β is a Bézout certificate for f and its
derivative, then every g whose coefficients differ from those of f by elements of order larger
than 2 v(β) has as many roots as f: each root of f lifts to a root of g close to it, and
conversely.
Three parts of the argument need no Henselian hypothesis and are stated separately. Two distinct
roots z ≠ z' of F satisfy v(z' − z) ≤ v(F'(z)), by the Taylor expansion of F at z;
the order of F' is constant on the ball v(y' − y) > v(F'(y)); and a root at distance of
order at least r ≥ d from x, with v(F'(x)) ≥ d, forces v(F(x)) ≥ r + d.
Main results #
Polynomial.eq_of_isRoot_of_addVal_lt: a root ofFcloser to a rootzthan the order ofF'(z)isz.Polynomial.addVal_derivative_eval_eq_of_lt: the order ofF'is constant on the ballv(y' − y) > v(F'(y)).Polynomial.le_addVal_eval_of_isRoot: a root in a ball of orderr ≥ dforces the value at its center to have order at leastr + d, if the derivative there has order at leastd.Polynomial.exists_isRoot_addVal_eval_eq: Hensel's lemma with an estimate, a rootzwithv(F(y₀)) = v(F'(y₀)) + v(z − y₀).Polynomial.existsUnique_isRoot_addVal_lt: that root is the unique root ofFin the ballv(z − y₀) > v(F'(y₀)).Polynomial.existsUnique_isRoot_le_addVal_iff: a closed ball of orderr > v(F'(y₀))contains exactly one root if and only ifr + v(F'(y₀)) ≤ v(F(y₀)).Polynomial.addVal_derivative_eval_le_of_lt: ifU F + V F' = β, the order ofF'is at mostv(β)whereverFhas order larger thanv(β).Polynomial.card_roots_le_of_eq_add_C_mul: a perturbationF + δ kofF, withδof order larger than twice that ofF'at each root ofF, has at least as many roots asF.Polynomial.card_roots_eq_of_addVal_lt_coeff_sub: a polynomial whose coefficients are close to those off, compared with a Bézout certificate forfandf', has as many roots asf.
Implementation notes #
Write d = F'(y₀). The polynomial F(y₀ + d X) has all its coefficients divisible by d²: its
constant coefficient F(y₀) by the hypothesis, its linear coefficient d · d, and its higher
coefficients through the factor dᵏ. The quotient G satisfies G(0) = F(y₀) / d² ∈ 𝔪 and
G'(0) = 1, so Hensel's lemma without monicity
(Polynomial.exists_isRoot_sub_mem) gives a root t ∈ 𝔪 of G.
Writing 0 = G(t) = G(0) + t + k t² shows v(t) = v(G(0)), which is the estimate for
z = y₀ + d t.
References #
- J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chap. II, §2.
Separation of roots. A root z' of F whose distance to a root z has order larger than
that of F'(z) is equal to z. Equivalently, two distinct roots z ≠ z' of F satisfy
addVal (z' - z) ≤ addVal (F'(z)).
The order of the derivative is constant on a ball whose radius exceeds it: if
addVal (F'(y)) < addVal (y' - y), then F'(y') and F'(y) have the same order.
The order of the derivative is bounded by a Bézout certificate. If U F + V F' = β, then
at every point where F has order larger than β (for instance at a root of F, when
β ≠ 0), the order of F' is at most that of β.
Hensel's lemma with an estimate over a Henselian discrete valuation ring. If the order of
F at y₀ exceeds twice the order of its derivative there, then F has a root z whose
distance to y₀ has order exactly addVal (F(y₀)) - addVal (F'(y₀)). This is the existence
part of Mathlib's hensels_lemma in addVal spelling; the uniqueness of z in that ball is
Polynomial.existsUnique_isRoot_addVal_lt.
Hensel's lemma with uniqueness over a Henselian discrete valuation ring. If the order of
F at y₀ exceeds twice the order of its derivative there, then F has exactly one root z
whose distance to y₀ has order larger than that of F'(y₀). Its distance to y₀ is given by
Polynomial.exists_isRoot_addVal_eval_eq.
A root in a ball of radius order r ≥ d forces the value at its center to have order
at least r + d, provided the derivative there has order at least d. No Henselian hypothesis
is needed, and infinite orders are allowed.
A closed ball strictly smaller than the derivative scale contains exactly one root
precisely when evaluation at its center has the corresponding extra order. Radius orders
may be extended naturals; order ⊤ gives the singleton ball {x}.
A small perturbation has at least as many roots. Let G = F + δ k be nonzero, where at
every root y of F the order of δ exceeds twice that of F'(y). Then G has at least as
many roots as F, counted with multiplicity.
Nearby polynomials have equally many roots. Let U f + V f' = β be a Bézout certificate
for f and its derivative over a Henselian discrete valuation ring. If every coefficient of
g - f has order larger than 2 v(β), then g has as many roots as f.