Valuations of polynomial expressions

A valuation takes value at most 1 on every polynomial expression in an element of value at most 1, provided the images of the coefficients also have value at most 1. Concretely, the ring of integers v.integer is a subring containing the images of the coefficients, so it contains every aeval t p with t in it; the proof below is the ultrametric bound on the coefficient sum, which is what Valuation supplies directly.

For the tautological valuation of a valuation subring containing a field of constants, a polynomial with nonzero constant term evaluated at an element of value less than 1 has value exactly 1: the constant term strictly dominates all the others. This is the polynomial estimate used in Stichtenoth's proof that valuation rings of algebraic function fields are discrete.

Finally, weighted coefficient bounds of the form v (P.coeff k * x ^ k) * S ^ a ≤ A ^ a * S ^ k are stable under products, powers and suitable composition, and bound the value of the polynomial at x. This controls truncated composites of power series.

Main results

• Valuation.aeval_le_one: v (Polynomial.aeval t p) ≤ 1 whenever v t ≤ 1 and the images of the coefficients have value at most 1.
• TauCeti.valuation_aeval_eq_one: a polynomial with nonzero constant term has value 1 when evaluated at an element of the maximal ideal of a valuation subring containing the coefficients.
• Valuation.map_coeff_mul_mul_pow_le, Valuation.map_coeff_pow_mul_pow_le, Valuation.map_coeff_comp_mul_pow_le, Valuation.map_eval_mul_le: weighted bounds on the terms of products, powers and composites of polynomials at a point, and the resulting bound on the value. They evaluate truncated composites of power series in nonarchimedean fields, such as the logarithm series after the exponential series.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0–1 infrastructure: the place-at-infinity argument for isogenies in AlgebraicGeometry/EllipticCurve/Isogeny/InfinityPlace.lean needs exactly this to see that a pulled-back affine function of a Weierstrass curve — a polynomial in the pulled-back coordinates — stays in the valuation ring at infinity. The statement is about a valuation and a polynomial and nothing else, so it is stated here rather than there.

TauCetiRoadmap/AlgebraicCurves/README.md, Layer 0: TauCeti.valuation_aeval_eq_one is the constant-term estimate used in Stichtenoth, Lemma 1.1.7, on the path to existence of places.

theorem Valuation.aeval_le_one {R : Type u_1} {L : Type u_2} {Γ₀ : Type u_3} [CommSemiring R] [Ring L] [Algebra R L] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation L Γ₀) (hR : ∀ (r : R), v ((algebraMap R L) r) ≤ 1) {t : L} (ht : v t ≤ 1) (p : Polynomial R) : v ((Polynomial.aeval t) p) ≤ 1

A valuation integral on the coefficients is at most 1 on polynomial expressions in an element of the integers.

Weighted coefficient bounds for products and compositions

Fix x, a scale A and a ratio S. Say that a polynomial P has weight a if v (P.coeff k * x ^ k) * S ^ a ≤ A ^ a * S ^ k for every k. Weights add under multiplication, so Q ^ n has weight n when Q has weight 1. If S ≤ 1, a polynomial of weight 1 whose coefficients below degree M vanish has v (P.eval x) * S ≤ A * S ^ M. When the coefficients of F satisfy v (F.coeff n) * A ^ n * S ≤ A * S ^ n, the composite F.comp Q has weight 1 whenever Q does. These bounds evaluate a truncated composite of two power series, such as the logarithm series after the exponential series, at a point of a nonarchimedean field.

theorem Valuation.map_coeff_mul_mul_pow_le {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} {x : R} {A S : Γ₀} {P Q : Polynomial R} {a b : ℕ} (hP : ∀ (k : ℕ), v (P.coeff k * x ^ k) * S ^ a ≤ A ^ a * S ^ k) (hQ : ∀ (k : ℕ), v (Q.coeff k * x ^ k) * S ^ b ≤ A ^ b * S ^ k) (k : ℕ) : v ((P * Q).coeff k * x ^ k) * S ^ (a + b) ≤ A ^ (a + b) * S ^ k

Weights add under multiplication of polynomials.

theorem Valuation.map_coeff_pow_mul_pow_le {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} {x : R} {A S : Γ₀} {Q : Polynomial R} (hQ : ∀ (k : ℕ), v (Q.coeff k * x ^ k) * S ≤ A * S ^ k) (n k : ℕ) : v ((Q ^ n).coeff k * x ^ k) * S ^ n ≤ A ^ n * S ^ k

The n-th power of a polynomial of weight 1 has weight n.

theorem Valuation.map_eval_mul_le {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀} {x : R} {A S : Γ₀} {G : Polynomial R} {M : ℕ} (hS : S ≤ 1) (hG₀ : ∀ k < M, G.coeff k = 0) (hG : ∀ (k : ℕ), v (G.coeff k * x ^ k) * S ≤ A * S ^ k) : v (Polynomial.eval x G) * S ≤ A * S ^ M

A polynomial of weight 1 whose coefficients vanish below degree M has v (G.eval x) * S ≤ A * S ^ M, provided S ≤ 1.

theorem Valuation.map_coeff_comp_mul_pow_le {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {x : R} {A S : Γ₀} {F Q : Polynomial R} (hF : ∀ (n : ℕ), v (F.coeff n) * A ^ n * S ≤ A * S ^ n) (hQ : ∀ (k : ℕ), v (Q.coeff k * x ^ k) * S ≤ A * S ^ k) (k : ℕ) : v ((F.comp Q).coeff k * x ^ k) * S ≤ A * S ^ k

Composition with a polynomial F whose coefficients satisfy v (F.coeff n) * A ^ n * S ≤ A * S ^ n preserves weight 1.

theorem TauCeti.valuation_aeval_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {A : ValuationSubring F} (hk : ∀ (c : k), (algebraMap k F) c ∈ A) {x : F} (hx : A.valuation x < 1) {p : Polynomial k} (hp : p.coeff 0 ≠ 0) : A.valuation ((Polynomial.aeval x) p) = 1

A polynomial with nonzero constant term, evaluated at a nonunit of a valuation subring containing the constants, is a unit: the constant term dominates.