Valuations of roots of monic polynomials

Elementary estimates for a valuation ν on a ring: a product of two ν-integral elements that is a ν-unit has ν-unit factors, and for a monic polynomial p with ν-integral coefficients the leading term dominates at any t with 1 < ν t, so that ν (p.eval t) = ν t ^ p.natDegree. Consequently, a root of such a polynomial has value at most one. These estimates do not require the ring to be commutative or the value monoid to have inverses.

Main results

• Valuation.eq_one_of_mul_eq_one: if ν a ≤ 1, ν b ≤ 1 and ν (a * b) = 1, then ν a = 1.
• Valuation.map_eval_eq_of_one_lt: ν (p.eval t) = ν t ^ p.natDegree for monic p with ν-integral coefficients and 1 < ν t.
• Valuation.le_one_of_root_monic: a root of a monic polynomial with ν-integral coefficients has value at most one.
• Valuation.map_quadratic_eq_of_one_lt and Valuation.one_lt_map_sq_add_mul_sub_iff: map_eval_eq_of_one_lt for the monic quadratic t² + at + c, and its consequence that t² + at - c has a pole exactly where t does — the x-coordinate λ² + a₁λ - a₂ - x₁ - x₂ of a chord sum, read in its slope λ.
• Valuation.map_cubic_eq_of_one_lt and Valuation.le_one_of_root_cubic: the two statements above for the monic cubic t³ + at² + bt + c, which is the shape a Weierstrass equation takes.

The cubic bounds apply to the Weierstrass equation: a root of the cubic is integral at every prime where its coefficients are integral. The companion estimate, for a polynomial expression in an element that is already integral, is TauCeti.RingTheory.Valuation.Polynomial.

Provenance

Adapted from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, commit 66889eada51a), EllipticCurves/Mathlib/Basic.lean, section Valuation, together with the cubic specializations from EllipticCurves/WeakMordellWeil.lean, section Cubic.

theorem Valuation.eq_one_of_mul_eq_one {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {a b : L} (ha : ν a ≤ 1) (hb : ν b ≤ 1) (hab : ν (a * b) = 1) : ν a = 1

If two elements have value at most one and their product has value one, then the first element has value one.

theorem Valuation.map_eval_eq_of_one_lt {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t : L} {p : Polynomial L} (hp : p.Monic) (hcoeff : ∀ i < p.natDegree, ν (p.coeff i) ≤ 1) (ht : 1 < ν t) : ν (Polynomial.eval t p) = ν t ^ p.natDegree

If p is monic with coefficients that are integral for the valuation ν and 1 < ν t, then the value of p at t is dominated by the leading term: ν (p.eval t) = ν t ^ p.natDegree. In particular, p.eval t ≠ 0.

theorem Valuation.le_one_of_root_monic {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t : L} {p : Polynomial L} (hp : p.Monic) (hcoeff : ∀ i < p.natDegree, ν (p.coeff i) ≤ 1) (heq : Polynomial.eval t p = 0) : ν t ≤ 1

A root of a monic polynomial whose coefficients have value at most one also has value at most one.

theorem Valuation.map_quadratic_eq_of_one_lt {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t a c : L} (ha : ν a ≤ 1) (hc : ν c ≤ 1) (ht : 1 < ν t) : ν (t ^ 2 + a * t + c) = ν t ^ 2

A monic quadratic with integral coefficients, evaluated at an element of value > 1, is dominated by its leading term.

theorem Valuation.one_lt_map_sq_add_mul_sub_iff {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t a c : L} (ha : ν a ≤ 1) (hc : ν c ≤ 1) : 1 < ν (t ^ 2 + a * t - c) ↔ 1 < ν t

A monic quadratic with integral coefficients has a pole exactly where its variable does: 1 < ν (t² + a t - c) if and only if 1 < ν t, for ν a ≤ 1 and ν c ≤ 1.

theorem Valuation.map_cubic_eq_of_one_lt {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t a b c : L} (ha : ν a ≤ 1) (hb : ν b ≤ 1) (hc : ν c ≤ 1) (ht : 1 < ν t) : ν (t ^ 3 + a * t ^ 2 + b * t + c) = ν t ^ 3

A monic cubic with integral coefficients, evaluated at an element of value > 1, is dominated by its leading term.

theorem Valuation.le_one_of_root_cubic {L : Type u_1} {Γ : Type u_2} [Ring L] [LinearOrderedCommMonoidWithZero Γ] (ν : Valuation L Γ) {t a b c : L} (ha : ν a ≤ 1) (hb : ν b ≤ 1) (hc : ν c ≤ 1) (heq : t ^ 3 + a * t ^ 2 + b * t + c = 0) : ν t ≤ 1

A root of a monic cubic with integral coefficients is integral.