Newton polygons under Weierstrass preparation

Let K be an ultrametric normed division ring (or field) whose norm comes from a real additive valuation v with base b > 1, so ‖x‖ = b ^ (-v x) for x ≠ 0. Weierstrass preparation on the closed disc of radius b ^ σ relates the Newton polygon of a series f up to its distinguished degree j to the Newton polygon of its polynomial factor P.

When f is distinguished of degree j at b ^ σ, u is a unit of the ring of series restricted at b ^ σ, and u * P = f for a polynomial P of degree at most j, the polynomial P has exact degree j, no outgoing finite edge at j, and up to the vertical shift v (u.coeff 0) the same Newton polygon as f at every index n ≤ j: f.newtonPolygon v n = P.newtonPolygon v n + v (u.coeff 0). Consequently the finite unit edges of P are the finite unit edges of f strictly below j, with identical unit slopes, and every finite Newton slope of P is at most σ. Global Minkowski additivity need not hold for a series restricted on only a single disc, so heights up to j are reconstructed from supporting values at slopes τ ≤ σ, where u remains distinguished of degree 0.

Conversely, a series restricted at b ^ σ whose Newton polygon has a finite face of slope σ ending at j touches its supporting line at the right endpoint j and is therefore distinguished of degree j at b ^ σ. When that face begins at the order of vanishing of f, every finite slope of P equals σ, giving the first-segment pure-polynomial case.

Main results

• Polynomial.Monic.isDistinguished_iff_forall_mem_newtonSlopes_le: a monic polynomial ω is distinguished in its full degree at b ^ σ if and only if all of its finite Newton slopes are at most σ.
• PowerSeries.isDistinguished_of_isFiniteFace: a series restricted at b ^ σ whose Newton polygon has a finite face of slope σ ending at j is distinguished of degree j at b ^ σ.
• PowerSeries.newtonPolygon_eq_add_of_isUnit_mul and PowerSeries.newtonPolygon_eq_of_mul_isUnit: f.newtonPolygon v n = P.newtonPolygon v n + v (u.coeff 0) for n ≤ j, reducing to equality when v (u.coeff 0) = 0.
• PowerSeries.notMem_finiteEdges_newtonPolygon_of_isUnit_mul, PowerSeries.mem_finiteEdges_newtonPolygon_iff_of_isUnit_mul and PowerSeries.unitSlope_newtonPolygon_eq_of_isUnit_mul: P has no outgoing finite edge at j and matches the finite unit edges and slopes of f strictly below j.
• PowerSeries.forall_mem_newtonSlopes_eq_of_isFiniteFace_of_order_eq and Polynomial.newtonSlopes_eq_filter_le_of_isFiniteFace: when a finite face of slope σ runs from the order of vanishing of f to j, any prepared polynomial factor P of degree at most j is pure of slope σ; for a polynomial f, any factor P prepared at a finite face (l, j) of slope σ has finite slope multiset (f.newtonSlopes v).filter (· ≤ σ).

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §4.
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, Grundlehren 261, Springer, 1984, §5.2.
• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, Publications Mathématiques de l'IHÉS 14 (1962), §§1, 3.

theorem Polynomial.le_of_mem_newtonSlopes_of_isDistinguished {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {P : Polynomial K} {σ : ℝ} (hPd : TauCeti.PowerSeries.IsDistinguished (b ^ σ) P.natDegree ↑P) {m : ℝ} (hm : m ∈ P.newtonSlopes v) : m ≤ σ

Every finite Newton slope of a polynomial P distinguished in its full degree at b ^ σ is at most σ.

theorem Polynomial.Monic.isDistinguished_iff_forall_mem_newtonSlopes_le {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {ω : Polynomial K} (hω : ω.Monic) {σ : ℝ} : TauCeti.PowerSeries.IsDistinguished (b ^ σ) ω.natDegree ↑ω ↔ ∀ s ∈ ω.newtonSlopes v, s ≤ σ

A monic polynomial ω is distinguished of degree ω.natDegree at b ^ σ if and only if all of its finite Newton slopes are at most σ.

theorem PowerSeries.notMem_finiteEdges_newtonPolygon_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) [IsUltrametricDist K] {f : PowerSeries K} {c : ℝ} (hc : 0 < c) {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished c j f) {u : ↥(IsRestricted.subring c)} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) : j ∉ TauCeti.finiteEdges (P.newtonPolygon v)

A polynomial factor P prepared at distinguished degree j has no outgoing finite edge at j.

theorem PowerSeries.isDistinguished_of_isFiniteFace {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : PowerSeries K} {σ : ℝ} {l j : ℕ} (hfr : IsRestricted (b ^ σ) f) (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l j) : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f

A power series restricted at b ^ σ whose Newton polygon has a finite face of slope σ ending at j is distinguished of degree j at b ^ σ.

theorem PowerSeries.supportingValue_newtonPolygon_eq_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ τ : ℝ} (hτσ : τ ≤ σ) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hmul : ↑u * ↑P = f) : TauCeti.supportingValue (f.newtonPolygon v) τ = (v ((coeff 0) ↑u)).toEReal + TauCeti.supportingValue (P.newtonPolygon v) τ

At every slope τ ≤ σ, the supporting value of f = u * P is v (u.coeff 0) plus that of P.

theorem PowerSeries.newtonPolygon_eq_add_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ : ℝ} {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) {n : ℕ} (hn : n ≤ j) : f.newtonPolygon v n = P.newtonPolygon v n + v ((coeff 0) ↑u)

Newton polygon of a prepared polynomial factor. Suppose f is distinguished of degree j at b ^ σ, u is a unit of the ring of series restricted at b ^ σ, and u * P = f for a polynomial P of degree at most j. Then for every n ≤ j, f.newtonPolygon v n = P.newtonPolygon v n + v (u.coeff 0).

theorem PowerSeries.mem_finiteEdges_newtonPolygon_iff_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ : ℝ} {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) (i : ℕ) : i ∈ TauCeti.finiteEdges (P.newtonPolygon v) ↔ i ∈ TauCeti.finiteEdges (f.newtonPolygon v) ∧ i < j

The finite unit edges of P are precisely the finite unit edges of f strictly below j.

theorem PowerSeries.unitSlope_newtonPolygon_eq_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ : ℝ} {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) {i : ℕ} (hi : i ∈ TauCeti.finiteEdges (f.newtonPolygon v)) (hij : i < j) : TauCeti.unitSlope (P.newtonPolygon v) i = TauCeti.unitSlope (f.newtonPolygon v) i

Every finite unit edge of f strictly below j has the same slope in P and in f.

theorem PowerSeries.le_of_mem_newtonSlopes_of_isUnit_mul {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ : ℝ} {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) {m : ℝ} (hm : m ∈ P.newtonSlopes v) : m ≤ σ

Every finite slope of a polynomial factor P prepared at b ^ σ is at most σ.

theorem PowerSeries.forall_mem_newtonSlopes_eq_of_isFiniteFace_of_order_eq {K : Type u_1} [NormedDivisionRing K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) [IsUltrametricDist K] {f : PowerSeries K} {σ : ℝ} {l j : ℕ} (hfr : IsRestricted (b ^ σ) f) (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l j) (hord : f.order = ↑l) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = f) (m : ℝ) : m ∈ P.newtonSlopes v → m = σ

First-segment pure-polynomial factorisation. If f is restricted at b ^ σ and its Newton polygon has a finite face of slope σ from its order of vanishing l (f.order = l) to j, then any polynomial factor P of degree at most j in u * P = f, with u a restricted unit at b ^ σ, is pure of slope σ.

theorem PowerSeries.newtonPolygon_eq_of_mul_isUnit {K : Type u_1} [NormedField K] [IsUltrametricDist K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : PowerSeries K} {σ : ℝ} {j : ℕ} (hf : TauCeti.PowerSeries.IsDistinguished (b ^ σ) j f) {u : ↥(IsRestricted.subring (b ^ σ))} (hu : IsUnit u) (hu0 : v ((coeff 0) ↑u) = 0) {P : Polynomial K} (hPdeg : P.natDegree ≤ j) (hmul : ↑P * ↑u = f) {n : ℕ} (hn : n ≤ j) : P.newtonPolygon v n = f.newtonPolygon v n

Newton polygon of a constant-normalised disc polynomial. When P * u = f with u a unit of the ring of series restricted at b ^ σ satisfying v (u.coeff 0) = 0 (for instance u.coeff 0 = 1), the Newton polygon of P equals that of f at every index n ≤ j.

theorem Polynomial.newtonSlopes_eq_filter_le_of_isFiniteFace {K : Type u_1} [NormedDivisionRing K] [IsUltrametricDist K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f P : Polynomial K} {σ : ℝ} {l j : ℕ} (hface : TauCeti.IsFiniteFace (f.newtonPolygon v) σ l j) {u : ↥(PowerSeries.IsRestricted.subring (b ^ σ))} (hu : IsUnit u) (hPdeg : P.natDegree ≤ j) (hmul : ↑u * ↑P = ↑f) : P.newtonSlopes v = Multiset.filter (fun (x : ℝ) => x ≤ σ) (f.newtonSlopes v)

Slopes of a polynomial factor prepared at a finite face. If f : K[X] has a finite face (l, j) of slope σ and (u : K⟦X⟧) * (P : K⟦X⟧) = (f : K⟦X⟧) for a restricted unit u at b ^ σ and a polynomial P of degree at most j, then the finite Newton slopes of P are precisely the finite Newton slopes of f that are at most σ.