Newton slopes, root valuations, and root norms

Let v be a real additive valuation for which only zero has infinite valuation. If a polynomial f splits into linear factors, its finite slope multiset Polynomial.newtonSlopes f v is the image of its multiset of nonzero roots under α ↦ -v α. This is the identification of the slopes of the Newton polygon with the negatives of the root valuations. The root zero, with multiplicity the order of vanishing of f at zero, contributes no slope.

The proof reads the slopes off the factorisation f = c * ∏ (X - α): the slopes of a product are the slopes of the factors together, and X - α has the single slope -v α when α ≠ 0 and no slope when α = 0. No completeness of the valuation is used. Applied after an extension of coefficients compatible with the valuations, this gives the slopes of a polynomial in terms of its roots in any valued extension in which it splits.

When v comes from an absolute value with ‖x‖ = b ^ (-v x) for a base 1 < b, the root α has norm b ^ m exactly when -v α = m. Hence the endpoints of the finite face of slope σ count the roots, with multiplicity and including the root zero, in the open and closed balls of radius b ^ σ, and the width of the face counts those on the sphere of that radius. Moreover, over an ultrametric normed field, every root of a nonzero pure polynomial of slope m in any normed field extension has norm at most b ^ m, and every nonzero root has norm b ^ m, without assuming that the polynomial splits.

Main results

• Polynomial.newtonSlopes_multiset_prod_X_sub_C: the finite slopes of ∏ (X - α) are the negated valuations of the nonzero α.
• Polynomial.newtonSlopes_eq_map_roots: the finite slopes of a split polynomial are the negated valuations of its nonzero roots.
• Polynomial.newtonSlopes_eq_map_roots_map: the same in a valued extension in which the polynomial splits.
• Polynomial.newtonSlopes_eq_replicate: if all nonzero roots have the same valuation -m, every finite slope equals m.
• Polynomial.neg_untop₀_mem_newtonSlopes_of_isRoot: the negated valuation of any nonzero root is a finite slope, without assuming that the polynomial splits.
• Polynomial.addValuation_eq_neg_of_forall_mem_newtonSlopes_eq: if every finite slope equals q, every nonzero root in a valued extension has valuation -q.
• Polynomial.card_filter_roots_lt_addValuation, Polynomial.card_filter_roots_le_addValuation and Polynomial.card_filter_roots_addValuation_eq: the left endpoint, the right endpoint and the width of the finite face of slope σ count the roots α with -σ < v α, with -σ ≤ v α and with v α = -σ.
• Polynomial.norm_le_rpow_of_forall_mem_newtonSlopes_eq and Polynomial.norm_eq_rpow_of_forall_mem_newtonSlopes_eq: over a normed field with norm b ^ (-v x), every root of a nonzero pure polynomial of slope m in any normed field extension has norm at most b ^ m, and every nonzero root has norm b ^ m.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3, Lemma 4.
• K. S. Kedlaya, Newton polygons, MIT 18.787, fall 2007, §1. Kedlaya plots coefficient points at negative indices; our convention uses positive indices, so the slopes have the opposite sign.

theorem Polynomial.newtonSlopes_multiset_prod_X_sub_C {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [DecidableEq R] (hv : ∀ (x : R), v x = ⊤ → x = 0) (s : Multiset R) : (Multiset.map (fun (x : R) => X - C x) s).prod.newtonSlopes v = Multiset.map (fun (α : R) => -(v α).untop₀) (Multiset.filter (fun (x : R) => x ≠ 0) s)

If only zero has infinite valuation, the finite slopes of ∏ (X - α), over a multiset of elements α, are the negated valuations -v α of the nonzero α, with multiplicity.

theorem Polynomial.neg_untop₀_mem_newtonSlopes_of_isRoot {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f ≠ 0) {α : R} (hα : α ≠ 0) (hroot : f.IsRoot α) : -(v α).untop₀ ∈ f.newtonSlopes v

If only zero has infinite valuation, the negated valuation -v α of a nonzero root α of a nonzero polynomial is one of its finite slopes. The polynomial need not split.

theorem Polynomial.addValuation_eq_neg_of_forall_mem_newtonSlopes_eq {K : Type u_2} {L : Type u_3} [Ring K] [CommRing L] {v : AddValuation K (WithTop ℝ)} {w : AddValuation L (WithTop ℝ)} (hw : ∀ (x : L), w x = ⊤ → x = 0) (φ : K →+* L) (hφ : ∀ (x : K), w (φ x) = v x) {f : Polynomial K} (hf : map φ f ≠ 0) {q : ℝ} (hq : ∀ m ∈ f.newtonSlopes v, m = q) {α : L} (hα : α ≠ 0) (hroot : (map φ f).IsRoot α) : w α = ↑(-q)

If every finite slope of f equals q, then every nonzero root α of f in a valued extension L whose valuation w restricts to v has valuation w α = -q. Only zero may have infinite valuation in L, and f need not split there.

theorem Polynomial.newtonSlopes_eq_map_roots {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] [DecidableEq R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) : f.newtonSlopes v = Multiset.map (fun (α : R) => -(v α).untop₀) (Multiset.filter (fun (x : R) => x ≠ 0) f.roots)

If only zero has infinite valuation, the finite slopes of a split polynomial are the negated valuations -v α of its nonzero roots α, with multiplicity. The root zero contributes no slope.

theorem Polynomial.newtonSlopes_eq_map_roots_map {K : Type u_2} {L : Type u_3} [Ring K] [CommRing L] [IsDomain L] [DecidableEq L] {v : AddValuation K (WithTop ℝ)} {w : AddValuation L (WithTop ℝ)} (hw : ∀ (x : L), w x = ⊤ → x = 0) (φ : K →+* L) (hφ : ∀ (x : K), w (φ x) = v x) {f : Polynomial K} (hf : (map φ f).Splits) : f.newtonSlopes v = Multiset.map (fun (α : L) => -(w α).untop₀) (Multiset.filter (fun (x : L) => x ≠ 0) (map φ f).roots)

If f splits over a valued extension L whose valuation w restricts to v, and only zero has infinite valuation in L, the finite slopes of f are the negated valuations -w α of its nonzero roots α in L, with multiplicity.

theorem Polynomial.newtonSlopes_eq_replicate {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) {m : ℝ} (hm : ∀ α ∈ f.roots, α ≠ 0 → v α = ↑(-m)) : f.newtonSlopes v = Multiset.replicate (f.natDegree - f.natTrailingDegree) m

If only zero has infinite valuation and all nonzero roots of a split polynomial have the same valuation -m, then every finite slope equals m: a polynomial of degree d and order of vanishing a at zero has the slope m with multiplicity d - a.

theorem Polynomial.card_filter_newtonSlopes_eq {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] [DecidableEq R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) (p : ℝ → Prop) [DecidablePred p] : (Multiset.filter p (f.newtonSlopes v)).card = (Multiset.filter (fun (α : R) => α ≠ 0 ∧ p (-(v α).untop₀)) f.roots).card

Counting finite slopes in terms of roots: a predicate holds for a number of finite slopes equal to the number of nonzero roots α for which it holds at -v α.

theorem Polynomial.card_filter_roots_lt_addValuation {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : (Multiset.filter (fun (α : R) => ↑(-σ) < v α) f.roots).card = l

If only zero has infinite valuation and f splits, the left endpoint of the finite face of slope σ of the Newton polygon is the number of roots α with -σ < v α, counted with multiplicity and including the root zero. For a valuation ‖x‖ = b ^ (-v x) with 1 < b, these are the roots in the open ball of radius b ^ σ.

theorem Polynomial.card_filter_roots_le_addValuation {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : (Multiset.filter (fun (α : R) => ↑(-σ) ≤ v α) f.roots).card = u

If only zero has infinite valuation and f splits, the right endpoint of the finite face of slope σ of the Newton polygon is the number of roots α with -σ ≤ v α, counted with multiplicity and including the root zero. For a valuation ‖x‖ = b ^ (-v x) with 1 < b, these are the roots in the closed ball of radius b ^ σ.

theorem Polynomial.card_filter_roots_addValuation_eq {R : Type u_1} [CommRing R] {v : AddValuation R (WithTop ℝ)} [IsDomain R] (hv : ∀ (x : R), v x = ⊤ → x = 0) {f : Polynomial R} (hf : f.Splits) {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : (Multiset.filter (fun (α : R) => v α = ↑(-σ)) f.roots).card = u - l

If only zero has infinite valuation and f splits, the width u - l of the finite face of slope σ of the Newton polygon is the number of roots α with v α = -σ, counted with multiplicity. For a valuation ‖x‖ = b ^ (-v x) with 1 < b, these are the roots on the sphere of radius b ^ σ.

theorem Polynomial.norm_le_rpow_of_forall_mem_newtonSlopes_eq {K : Type u_1} {L : Type u_2} [NormedField K] [NormedField L] [NormedAlgebra K L] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf : f ≠ 0) {m : ℝ} (hm : ∀ s ∈ f.newtonSlopes v, s = m) {x : L} (hx : (aeval x) f = 0) : ‖x‖ ≤ b ^ m

Every root x of a nonzero polynomial pure of slope m, in any normed field extension L of K, satisfies ‖x‖ ≤ b ^ m.

theorem Polynomial.norm_eq_rpow_of_forall_mem_newtonSlopes_eq {K : Type u_1} {L : Type u_2} [NormedField K] [NormedField L] [NormedAlgebra K L] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf : f ≠ 0) {m : ℝ} (hm : ∀ s ∈ f.newtonSlopes v, s = m) {x : L} (hx0 : x ≠ 0) (hx : (aeval x) f = 0) : ‖x‖ = b ^ m

Every nonzero root x of a nonzero polynomial pure of slope m, in any normed field extension L of K, has norm ‖x‖ = b ^ m.