Auxiliary file: quantitative root-lifting #
The analytic engine behind equation (3) and Lemma 1 of §3: a simple root of a monic integral
polynomial lifts to a root of every coefficientwise-close monic integral polynomial, inside any L
in sigma K n ([Serre 1978, Lemma 1, pp.1032–1033][Serre1978]). The concluding theorem
card_aroots_eq states the consequence used downstream: for a separable monic f over 𝒪[K],
there is a threshold T such that every monic g with g.coeff i - f.coeff i in the T-th power
of 𝓂[K] for all i has exactly as many roots in L as f does—the local constancy of the root
count, which First.lean restates on the Eisenstein region and which the measurability,
countability, and change-of-variables arguments downstream consume.
The route is Newton–Hensel over the complete ring integers L, organized in four layers:
- The
proof_wantedof Mathlib.isAdicComplete_integerprovesIsAdicComplete 𝓂[K] 𝒪[K]—stated asproof_wanted isAdicCompleteinMathlib/NumberTheory/LocalField/Basic.lean—withIsHausdorfffrom the Krull intersection theorem andIsPrecompletefrom Cantor's intersection of the nested closed balls around the partial terms, inside the compact unit ball ofK. - The structure of
integers Lat an Eisenstein generator. Through the monogenic presentation ofintegers_eq_adjoin,integers Lis𝒪[K][X]modulo(G): free of ranknover𝒪[K](basisOfEisenstein), local with maximal ideal generated by the root (isMaximal_span_integralGen,isLocalRing_integers), a discrete valuation ring (isDiscreteValuationRing_integers), and adically complete (isAdicComplete_span_integralGen)—completeness transfers coefficientwise along the basis, and the interleaving of(ξ) ^ nwithπtimesintegers Lconverts𝓂[K]-adic limits into(ξ)-adic ones. - Newton iteration.
exists_isRootis the quantitative Hensel lemma over an abstract complete discrete valuation ring: if the order ofFaty₀exceeds twice that of its derivative, the iteration sendingytoy - F y / F' yconverges to a rootzwhose distance toy₀has order at least the difference of the two. - The count comparison. A Bézout certificate
U * f + V * f' = βover𝒪[K](from separability overK, denominators cleared byIsLocalization.integerNormalization) bounds the order of the derivative offat every near-root by the orderΓofβ, uniformly; with thresholdT = 2 * Γ + 1, Newton lifts each root of either polynomial to a root of the other at distance of order greater thanΓ, while distinct roots stay at distance of order at mostΓ—so the two lifting maps are injective, every root inLis simple, and the counts agree.
No topology on L enters anywhere: the completeness of integers L is the algebraic
IsAdicComplete, and all estimates use the ℕ∞-valued IsDiscreteValuationRing.addVal of
integers L.
References #
- [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.
The proof_wanted of Mathlib: 𝒪[K] is 𝓂[K]-adically complete #
The ring of integers of a nonarchimedean local field is complete for its maximal-adic
topology—the statement proof_wanted isAdicComplete of
Mathlib/NumberTheory/LocalField/Basic.lean. IsHausdorff is the Krull intersection theorem in the
Noetherian local ring 𝒪[K]; for IsPrecomplete, the closed balls around the partial terms of a
coherent sequence, of radius the j-th power of the valuation of π, are nested nonempty closed
subsets of the compact unit ball of K, so Cantor's intersection theorem provides the limit.
Adic completeness of finite free modules, coefficientwise #
The structure of the integral closure at an Eisenstein generator #
Everything below is relative to a root x of an Eisenstein polynomial over 𝒪[K], through the
monogenic presentation of integers_eq_adjoin: writing G for minpoly 𝒪[K] x and n for its
degree, the integral closure of 𝒪[K] in K⟮x⟯ is 𝒪[K][ξ], presented as 𝒪[K][X] modulo (G),
a complete discrete valuation ring with maximal ideal (ξ) and (ξ) ^ n equal to π times that
closure.
The generator x of K⟮x⟯, seen inside the integral closure—the canonical lift of
IntermediateField.AdjoinSimple.gen K x.
Equations
Instances For
The minimal polynomial vanishes at integralGen, in the eval₂ form AdjoinRoot.liftAlgHom
demands.
The monogenic presentation read as an algebra map out of AdjoinRoot: substitution of
integralGen for the root.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presentation is bijective: injective because the kernel of evaluation is exactly (G),
surjective by the monogenicity of integers_eq_adjoin.
The monogenic presentation, identifying 𝒪[K][X] modulo (G) with integers L, as an algebra
equivalence.
Equations
- MassFormula.adjoinRootEquiv hπ hint hei = AlgEquiv.ofBijective (MassFormula.adjoinRootLift hint) ⋯
Instances For
The presentation carries the root of AdjoinRoot to the Eisenstein generator.
The integral closure as a power basis over 𝒪[K], generated by the Eisenstein generator: the
presentation of integers L as 𝒪[K][X] modulo (G) carries the power basis of AdjoinRoot
across.
Equations
- MassFormula.powerBasisOfEisenstein hπ hint hei = (AdjoinRoot.powerBasis' ⋯).map (MassFormula.adjoinRootEquiv hπ hint hei)
Instances For
The power basis of the integral closure over 𝒪[K], on the index type Fin n of the minimal
polynomial's degree. Its i-th element is ξ ^ i (basisOfEisenstein_apply);
UniformizerParam.lean reads the coordinates of integers L off it.
Equations
- MassFormula.basisOfEisenstein hπ hint hei = (MassFormula.powerBasisOfEisenstein hπ hint hei).basis
Instances For
The power basis is the basis of the powers of the Eisenstein generator.
The ideal generated by integralGen is maximal—via the presentation of integers L as
𝒪[K][X] modulo (G) and the residue map at the constant coefficient.
Every maximal ideal of the integral closure is (integralGen): it lies over 𝓂[K], hence
contains the constant coefficient, hence—by the Eisenstein unit relation—the generator.
The integral closure is local: (integralGen) is its unique maximal ideal.
The interleaving identity equating (ξ) ^ n with π times the integral closure, from the
Eisenstein unit relation c₀ * u = -ξ ^ n and the association of c₀ with π.
The integral closure is a discrete valuation ring: local by isLocalRing_integers, Dedekind by
Krull–Akizuki, not a field since integralGen ≠ 0 generates the maximal ideal.
The integral closure is complete for its maximal-adic topology.
IsHausdorff is Krull intersection; for IsPrecomplete, a coherent sequence for the powers of
(integralGen) is, along the subsequence of indices n * m, coherent for the powers of 𝓂[K]—by
the interleaving of (ξ) ^ n with π times the integral closure—and the free module 𝒪[K]-basis
of basisOfEisenstein produces the limit coefficientwise from isAdicComplete_integer.
Quantitative Newton iteration over a complete discrete valuation ring #
Quantitative Newton–Hensel over a complete discrete valuation ring: a point where F vanishes
to order more than twice that of its derivative converges under the Newton iteration to an exact
root, at distance of order the difference of the two. The conclusion is stated additively—the order
of F at y₀ is at most that of its derivative plus that of z - y₀—to stay subtraction-free in
ℕ∞.
The form of the Newton lemma used by the count comparison: at a point where F vanishes to
order at least 2 * Γ + 1 while its derivative has order at most Γ, there is a root at distance
of order at least Γ + 1.
Root separation: two distinct roots of a polynomial lie no closer than the order of the
derivative at either—from the factorization F = (X - y) * q, the identity giving the derivative
at y as q evaluated at y, and the divisibility of q y - q y' by y - y'.
Elements of (ϖa ^ T) have order at least T, once ϖa has positive order.
A polynomial with all coefficients in (ϖa ^ T) evaluates into (ϖa ^ T).
The Bézout certificate of separability and the count comparison #
A polynomial separable over the fraction field K admits a Bézout certificate over 𝒪[K]
itself: U * f + V * f' = β with β ≠ 0, by clearing the denominators of a coprimality witness.
Quantitative root-lifting, the analytic engine behind equation (3) and Lemma 1 of §3: for L
in sigma K n and a monic f over 𝒪[K] separable over K, there is a threshold 0 < T such
that every monic g with all coefficients congruent to those of f modulo the T-th power of
𝓂[K] has exactly as many roots in L, with multiplicity, as f
([Serre 1978, Lemma 1, pp.1032–1033][Serre1978]). With Γ the valuation in integers L of the
Bézout constant of f and T = 2 * Γ + 1: at any root of either polynomial the Bézout identity
pins the derivative order at at most Γ, so Newton (exists_isRoot_near) lifts each root of either
polynomial to a root of the other at distance of order greater than Γ, while distinct roots of one
polynomial stay at distance of order at most Γ (addVal_sub_le_of_isRoot); the liftings are
therefore injective both ways, and every root in L is simple, so the counts agree.