Finite slopes of the Newton polygon of a polynomial

The Newton polygon of a polynomial has finitely many finite unit edges. Its finite slope multiset Polynomial.newtonSlopes f v lists the slopes of these edges, with multiplicity. With the orientation of Polynomial.newtonPolygon, a slope m corresponds to a nonzero root of valuation -m; for a linear polynomial X - C α with v α finite this is Polynomial.newtonSlopes_X_sub_C. These multisets are the invariants in which the slopes of products and of split polynomials are stated.

A polynomial f is pure of slope m when every finite slope of its Newton polygon equals m. Write a for the order of vanishing of f at zero and d for its degree. If the trailing and leading coefficients have finite valuation, the polygon runs from the trailing point (a, v (coeff a f)) to the leading point (d, v (coeff d f)), so purity says that the polygon is the segment joining these two points. Purity of slope m is therefore equivalent to two conditions on the coefficients: the line of slope m through the trailing point passes through the leading point, and every coefficient point lies on or above that line. Interior coefficient points may lie on the line; for instance 1 + p X + p ^ 2 X ^ 2 is pure of slope 1 for the p-adic valuation. The basic example is an Eisenstein polynomial: if the leading coefficient of f has valuation zero, its constant coefficient has valuation one and its other coefficients below the degree have valuation at least one, then its polygon is the segment from (0, 1) to (d, 0) and every finite slope equals -1 / d.

The multiset depends only on the polygon. Whenever the polygon is nonempty it is represented by finite slope data, and the finite slope multiset is the slope multiset of that presentation, so the geometric results about TauCeti.FiniteSlopeData.slopeMultiset apply.

Main definitions

• Polynomial.newtonSlopes f v: the multiset of the slopes of the finite unit edges of f.newtonPolygon v.

Main results

• Polynomial.newtonSlopes_eq_slopeMultiset: the finite slope multiset is the slope multiset of any finite slope data representing the Newton polygon, and by Polynomial.exists_finiteSlopeData_heights_eq_iff such data exists exactly when the polygon is nonempty.
• Polynomial.card_newtonSlopes: if only zero has infinite valuation, a polynomial of degree d and order of vanishing a at zero has d - a finite slopes.
• Polynomial.sum_newtonSlopes: their sum is the difference between the valuations of the leading and trailing coefficients.
• Polynomial.den_dvd_card_newtonSlopes: for a valuation taking integer values on nonzero elements, if every finite slope equals the rational q, then the denominator of q divides the number of finite slopes.
• Polynomial.exists_isFiniteFace_newtonPolygon: a nonempty Newton polygon has a finite face of every real slope.
• Polynomial.count_newtonSlopes_of_isFiniteFace: the multiplicity of a slope σ is the width of the face of slope σ.
• Polynomial.left_eq_natTrailingDegree_add_card_filter_newtonSlopes_lt and Polynomial.right_eq_natTrailingDegree_add_card_filter_newtonSlopes_le: the absolute endpoints of the face of slope σ are the order of vanishing at zero plus the number of finite slopes below σ, respectively at most σ.
• Polynomial.newtonSlopes_C_mul, Polynomial.newtonSlopes_X_pow_mul, Polynomial.newtonSlopes_comp_C_mul_X and Polynomial.newtonSlopes_map: multiplication by a scalar of finite valuation and by X ^ k preserves the slopes, the substitution X ↦ c X adds the valuation of c to every slope, and an extension of coefficients compatible with the valuations preserves them. By Polynomial.newtonSlopes_map_eq_map_mul, an extension of coefficients multiplying the valuations by a positive real factor multiplies the slopes by that factor.
• Polynomial.newtonSlopes_reflect and Polynomial.newtonSlopes_reverse: reversing the coefficients negates the finite slopes.
• Polynomial.newtonSlopes_monomial: a monomial, in particular a constant, has no finite slopes.
• Polynomial.newtonSlopes_X_sub_C: the only finite slope of X - C α is -v α.
• Polynomial.forall_mem_newtonSlopes_eq_iff: the purity criterion. If the trailing and leading coefficients have finite valuation, every finite slope equals m exactly when the leading point lies on the line of slope m through the trailing point and no coefficient point lies below that line.
• Polynomial.newtonSlopes_eq_replicate_of_eisenstein: an Eisenstein polynomial of degree d has d finite slopes, all equal to -1 / d.

References

• J. Neukirch, Algebraic Number Theory, Grundlehren 322, Springer, 1999, Chapter II §6, Proposition 6.3 and its corollary.
• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §3.

theorem Polynomial.finite_finiteEdges_newtonPolygon {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : (TauCeti.finiteEdges (f.newtonPolygon v)).Finite

The Newton polygon of a polynomial has only finitely many finite unit edges, all before the degree.

noncomputable def Polynomial.newtonSlopes {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : Multiset ℝ

The finite slope multiset of the Newton polygon of a polynomial: the slopes of all of its finite unit edges, counted with multiplicity. The zero polynomial has no finite slopes.

theorem Polynomial.newtonSlopes_def {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.newtonSlopes v = Multiset.map (TauCeti.unitSlope (f.newtonPolygon v)) ⋯.toFinset.val

The finite slope multiset is the image of the finite unit edges under their slopes.

@[simp]

theorem Polynomial.mem_newtonSlopes {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {m : ℝ} : m ∈ f.newtonSlopes v ↔ ∃ n ∈ TauCeti.finiteEdges (f.newtonPolygon v), TauCeti.unitSlope (f.newtonPolygon v) n = m

A real number is a finite slope exactly when it is the slope of a finite unit edge.

theorem Polynomial.newtonSlopes_eq_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : Polynomial S} {w : AddValuation S (WithTop ℝ)} {φ : ℕ → ℕ} (hφ : Set.InjOn φ (TauCeti.finiteEdges (f.newtonPolygon v))) {t : ℝ → ℝ} (hedges : TauCeti.finiteEdges (g.newtonPolygon w) = φ '' TauCeti.finiteEdges (f.newtonPolygon v)) (hslope : ∀ n ∈ TauCeti.finiteEdges (f.newtonPolygon v), TauCeti.unitSlope (g.newtonPolygon w) (φ n) = t (TauCeti.unitSlope (f.newtonPolygon v) n)) : g.newtonSlopes w = Multiset.map t (f.newtonSlopes v)

Transport of finite slopes along a matching of finite unit edges.

theorem Polynomial.newtonSlopes_congr {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : Polynomial S} {w : AddValuation S (WithTop ℝ)} (h : f.newtonPolygon v = g.newtonPolygon w) : f.newtonSlopes v = g.newtonSlopes w

The finite slope multiset depends only on the Newton polygon.

theorem Polynomial.newtonSlopes_eq_slopeMultiset {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {d : TauCeti.FiniteSlopeData ℝ} (hd : d.heights = f.newtonPolygon v) : f.newtonSlopes v = d.slopeMultiset

The finite slope multiset is the slope multiset of any finite slope data representing the Newton polygon.

theorem Polynomial.exists_finiteSlopeData_heights_eq_iff {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : (∃ (d : TauCeti.FiniteSlopeData ℝ), d.heights = f.newtonPolygon v) ↔ f.newtonPolygon v ≠ ⊤

The Newton polygon of a polynomial is represented by finite slope data exactly when it is nonempty.

theorem Polynomial.exists_isFiniteFace_newtonPolygon {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hf : f.newtonPolygon v ≠ ⊤) (σ : ℝ) : ∃ (l : ℕ) (u : ℕ), TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u

A nonempty Newton polygon of a polynomial has a finite face of every real slope σ. The endpoints are absolute indices.

theorem Polynomial.count_newtonSlopes_of_isFiniteFace {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : Multiset.count σ (f.newtonSlopes v) = u - l

The multiplicity of a real slope σ among the finite slopes is the width u - l of the finite face of slope σ. The endpoints l and u are absolute indices, and a singleton face contributes multiplicity zero.

theorem Polynomial.card_filter_newtonSlopes {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (p : ℝ → Prop) [DecidablePred p] : (Multiset.filter p (f.newtonSlopes v)).card = {i : ℕ | i ∈ TauCeti.finiteEdges (f.newtonPolygon v) ∧ p (TauCeti.unitSlope (f.newtonPolygon v) i)}.ncard

The number of finite slopes satisfying a predicate is the number of finite unit edges whose slope satisfies it.

theorem Polynomial.left_eq_natTrailingDegree_add_card_filter_newtonSlopes_lt {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hv : ∀ (x : R), v x = ⊤ → x = 0) {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : l = f.natTrailingDegree + (Multiset.filter (fun (x : ℝ) => x < σ) (f.newtonSlopes v)).card

If only zero has infinite valuation, the left endpoint of the finite face of slope σ is the order of vanishing at zero plus the number of finite slopes strictly less than σ. The endpoint is an absolute index.

theorem Polynomial.right_eq_natTrailingDegree_add_card_filter_newtonSlopes_le {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hv : ∀ (x : R), v x = ⊤ → x = 0) {σ : ℝ} {l u : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l u) : u = f.natTrailingDegree + (Multiset.filter (fun (x : ℝ) => x ≤ σ) (f.newtonSlopes v)).card

If only zero has infinite valuation, the right endpoint of the finite face of slope σ is the order of vanishing at zero plus the number of finite slopes at most σ. The endpoint is an absolute index.

Length and total height change

theorem Polynomial.card_newtonSlopes {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (hv : ∀ (x : R), v x = ⊤ → x = 0) : (f.newtonSlopes v).card = f.natDegree - f.natTrailingDegree

If only zero has infinite valuation, a polynomial of degree d and order of vanishing a at zero has exactly d - a finite slopes, counted with multiplicity.

theorem Polynomial.sum_newtonSlopes {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (hv : ∀ (x : R), v x = ⊤ → x = 0) : (f.newtonSlopes v).sum = (v f.leadingCoeff).untop₀ - (v f.trailingCoeff).untop₀

If only zero has infinite valuation, the sum of the finite slopes of a polynomial is the valuation of its leading coefficient minus that of its trailing coefficient.

theorem Polynomial.den_dvd_card_newtonSlopes {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hint : ∀ (x : R), x ≠ 0 → ∃ (n : ℤ), v x = ↑↑n) {q : ℚ} (hf : ∀ m ∈ f.newtonSlopes v, m = ↑q) : q.den ∣ (f.newtonSlopes v).card

If the valuation takes integer values on nonzero elements and every finite slope of f equals the rational number q, then the denominator of q divides the number of finite slopes of f, that is, the horizontal length of its Newton polygon.

Elementary operations

@[simp]

theorem Polynomial.newtonSlopes_monomial {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) (k : ℕ) (c : R) : ((monomial k) c).newtonSlopes v = 0

A monomial, in particular a constant, has no finite slopes.

@[simp]

theorem Polynomial.newtonSlopes_zero {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) : newtonSlopes 0 v = 0

The zero polynomial has no finite slopes.

@[simp]

theorem Polynomial.newtonSlopes_C {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) (c : R) : (C c).newtonSlopes v = 0

A constant polynomial has no finite slopes.

theorem Polynomial.newtonSlopes_C_mul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {c : R} (hc : v c ≠ ⊤) : (C c * f).newtonSlopes v = f.newtonSlopes v

Multiplying by a constant of finite valuation preserves the finite slopes.

theorem Polynomial.newtonSlopes_smul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {c : R} (hc : v c ≠ ⊤) : (c • f).newtonSlopes v = f.newtonSlopes v

Multiplying by a scalar of finite valuation preserves the finite slopes.

@[simp]

theorem Polynomial.newtonSlopes_X_pow_mul {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (k : ℕ) : (X ^ k * f).newtonSlopes v = f.newtonSlopes v

Multiplying by X ^ k preserves the finite slopes.

theorem Polynomial.newtonSlopes_comp_C_mul_X {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {c : R} (hc : v c ≠ ⊤) : (f.comp (C c * X)).newtonSlopes v = Multiset.map (fun (x : ℝ) => x + (v c).untop₀) (f.newtonSlopes v)

Substituting c X for X adds the valuation of c to every finite slope, provided that valuation is finite.

theorem Polynomial.newtonSlopes_reflect {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) {N : ℕ} (hN : f.natDegree ≤ N) : (reflect N f).newtonSlopes v = Multiset.map Neg.neg (f.newtonSlopes v)

Reflecting the coefficients in an index N at least the degree negates the finite slopes. The order of the slopes is reversed, which a multiset does not record.

@[simp]

theorem Polynomial.newtonSlopes_reverse {R : Type u_1} [Ring R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) : f.reverse.newtonSlopes v = Multiset.map Neg.neg (f.newtonSlopes v)

Reversing a polynomial negates its finite slopes.

theorem Polynomial.newtonSlopes_map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} (hφ : ∀ (x : R), w (φ x) = v x) : (map φ f).newtonSlopes w = f.newtonSlopes v

Mapping the coefficients along a ring homomorphism compatible with the valuations preserves the finite slopes.

theorem Polynomial.newtonSlopes_map_eq_map_mul {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} {c : ℝ} (hc : 0 < c) (hφ : ∀ (x : R), w (φ x) = WithTop.map (fun (x : ℝ) => c * x) (v x)) : (map φ f).newtonSlopes w = Multiset.map (fun (x : ℝ) => c * x) (f.newtonSlopes v)

Mapping the coefficients along a ring homomorphism that multiplies the valuations by a positive real factor multiplies every finite slope by that factor.

Linear polynomials

theorem Polynomial.newtonSlopes_X_sub_C {R : Type u_1} [Ring R] (v : AddValuation R (WithTop ℝ)) {α : R} (hα : v α ≠ ⊤) : (X - C α).newtonSlopes v = {-(v α).untop₀}

The polynomial X - C α, whose root α has finite valuation, has the single finite slope -v α.

Pure polynomials

theorem Polynomial.forall_mem_newtonSlopes_eq_iff {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (htr : v f.trailingCoeff ≠ ⊤) (hld : v f.leadingCoeff ≠ ⊤) {m : ℝ} : (∀ s ∈ f.newtonSlopes v, s = m) ↔ (v f.leadingCoeff).untop₀ = (v f.trailingCoeff).untop₀ + m * (↑f.natDegree - ↑f.natTrailingDegree) ∧ ∀ (n : ℕ), ↑((v f.trailingCoeff).untop₀ + m * (↑n - ↑f.natTrailingDegree)) ≤ v (f.coeff n)

Purity criterion. If the trailing and leading coefficients of f have finite valuation, every finite slope of f equals m exactly when the line of slope m through the trailing point (a, v (coeff a f)), where a is the order of vanishing of f at zero, passes through the leading point and lies on or below every coefficient point.

theorem Polynomial.newtonSlopes_eq_replicate_of_eisenstein {R : Type u_1} [Ring R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hlead : v f.leadingCoeff = 0) (h0 : v (f.coeff 0) = 1) (hmem : ∀ (n : ℕ), 0 < n → n < f.natDegree → 1 ≤ v (f.coeff n)) : f.newtonSlopes v = Multiset.replicate f.natDegree (-(↑f.natDegree)⁻¹)

Eisenstein polygons. If f has leading coefficient of valuation zero, constant coefficient of valuation one, and all other coefficients below the degree of valuation at least one, then the Newton polygon of f is the segment from (0, 1) to (d, 0), where d is the degree of f: it has d finite slopes, all equal to -1 / d.