Pure slope factorisations of polynomials and restricted power series

Over any field K equipped with v : AddValuation K (WithTop ℝ), nonzero polynomials not both vanishing at 0 whose finite Newton slope multisets are disjoint are coprime. A pure slope factorisation Polynomial.IsPureSlopeFactorization f v g represents a constant-one polynomial f as a finitely supported product ∏ᶠ m, g m of constant-one polynomials g m each pure of slope m. Purity and the constant-term normalisation force (g m).natDegree = (f.newtonSlopes v).count m and g m = 1 outside f.newtonSlopes v, making g unique over any field.

When K is a complete ultrametric normed field whose norm comes from v with base b > 1, peeling off the finite face at any slope threshold σ via Weierstrass preparation (TauCeti.NumberTheory.NewtonPolygon.Weierstrass) and polynomial divisibility reflection (TauCeti.PowerSeries.IsDistinguished.polynomialToRestricted_dvd_iff) constructs g over K itself, with no splitting or discreteness hypothesis. In particular, any polynomial over K whose finite Newton slopes have multiplicity one splits into linear factors over K.

Combining Weierstrass preparation on any closed disc of positive radius with the pure slope factorisation of its preparation polynomial factors any nonzero restricted power series on that disc into a restricted unit, X ^ a for its order a at zero (PowerSeries.order_eq_of_isUnit_X_pow_mul_finprod_eq), and unique pairwise coprime constant-one pure polynomial factors of slopes within the disc. In any complete normed field extension L of K, the zeros of the series on the sphere ‖x‖ = b ^ m inside the disc are precisely the roots of the slope-m factor.

Main definitions

• Polynomial.IsPureSlopeFactorization f v g: g : ℝ → R[X] has finite multiplicative support, each g m has constant coefficient 1 and all finite Newton slopes equal to m, and ∏ᶠ m, g m = f.

Main results

• Polynomial.isCoprime_of_disjoint_newtonSlopes and Polynomial.isCoprime_of_forall_mem_newtonSlopes_eq: nonzero polynomials over a field with disjoint finite slopes (not both vanishing at 0) are coprime.
• Polynomial.IsPureSlopeFactorization.natDegree_apply, Polynomial.IsPureSlopeFactorization.mulSupport_eq, Polynomial.IsPureSlopeFactorization.pairwise_isCoprime and Polynomial.IsPureSlopeFactorization.unique: degree determination, support, pairwise coprimality and uniqueness of pure slope factorisations.
• Polynomial.exists_mul_newtonSlopes_filter_le: threshold factorisation f = P * Q separating finite slopes ≤ σ from finite slopes > σ.
• Polynomial.existsUnique_isPureSlopeFactorization, Polynomial.existsUnique_C_mul_finprod_eq and Polynomial.existsUnique_C_mul_X_pow_mul_finprod_eq: existence and uniqueness of the pure slope factorisation over a complete ultrametric normed field.
• Polynomial.splits_of_nodup_newtonSlopes: a polynomial over a complete ultrametric normed field with distinct finite Newton slopes splits over the base field.
• PowerSeries.existsUnique_isUnit_X_pow_mul_finprod_eq, PowerSeries.existsUnique_isUnit_X_pow_mul_finprod_eq_of_pos and PowerSeries.setOf_norm_eq_and_evalAt_eq_zero: closed-disc pure slope factorisation of a restricted power series and sphere-by-sphere identification of its zeros.

References

• N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, second edition, Graduate Texts in Mathematics 58, Springer, 1984, Chapter IV §§3–4.
• K. S. Kedlaya, Newton polygons, MIT 18.787, fall 2007, §§1–2.
• 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.

Slope coprimality and pure slope factorisations

theorem Polynomial.isCoprime_of_disjoint_newtonSlopes {K : Type u_1} [Field K] (v : AddValuation K (WithTop ℝ)) {f g : Polynomial K} (hf : f ≠ 0) (hg : g ≠ 0) (h0 : f.coeff 0 ≠ 0 ∨ g.coeff 0 ≠ 0) (hdisj : Disjoint (f.newtonSlopes v) (g.newtonSlopes v)) : IsCoprime f g

Over a field, two nonzero polynomials not both vanishing at zero whose finite Newton slope multisets are disjoint are coprime.

theorem Polynomial.isCoprime_of_forall_mem_newtonSlopes_eq {K : Type u_1} [Field K] (v : AddValuation K (WithTop ℝ)) {f g : Polynomial K} (hf : f ≠ 0) (hg : g ≠ 0) (h0 : f.coeff 0 ≠ 0 ∨ g.coeff 0 ≠ 0) {m₁ m₂ : ℝ} (hm₁ : ∀ s ∈ f.newtonSlopes v, s = m₁) (hm₂ : ∀ s ∈ g.newtonSlopes v, s = m₂) (hne : m₁ ≠ m₂) : IsCoprime f g

Over a field, two nonzero pure polynomials of distinct slopes m₁ ≠ m₂, not both vanishing at zero, are coprime.

structure Polynomial.IsPureSlopeFactorization {R : Type u_1} [CommRing R] (f : Polynomial R) (v : AddValuation R (WithTop ℝ)) (g : ℝ → Polynomial R) : Prop

A family g : ℝ → R[X] is a pure slope factorisation of f for v if g has finite multiplicative support, each g m has constant coefficient 1 and all finite Newton slopes equal to m, and ∏ᶠ m, g m = f.

• finite_mulSupport : (Function.mulSupport g).Finite

  Only finitely many factors g m differ from 1.

• coeff_zero (m : ℝ) : (g m).coeff 0 = 1

  Every factor is normalised to have constant coefficient 1.

• newtonSlopes_eq (m s : ℝ) : s ∈ (g m).newtonSlopes v → s = m

  Every finite Newton slope of g m equals m.

• finprod_eq : ∏ᶠ (m : ℝ), g m = f

  The finite product of the family g recovers f.

theorem Polynomial.isPureSlopeFactorization_iff {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} : f.IsPureSlopeFactorization v g ↔ (Function.mulSupport g).Finite ∧ (∀ (m : ℝ), (g m).coeff 0 = 1) ∧ (∀ (m s : ℝ), s ∈ (g m).newtonSlopes v → s = m) ∧ ∏ᶠ (m : ℝ), g m = f

Unfolded characterisation of Polynomial.IsPureSlopeFactorization.

theorem Polynomial.IsPureSlopeFactorization.coeff_zero_eq_one {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) : f.coeff 0 = 1

A polynomial admitting a pure slope factorisation has constant coefficient 1.

theorem Polynomial.IsPureSlopeFactorization.apply_ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) (m : ℝ) : g m ≠ 0

The existence of a real additive valuation makes the coefficient ring nontrivial, so every factor g m is nonzero.

theorem Polynomial.IsPureSlopeFactorization.ne_zero {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) : f ≠ 0

A polynomial admitting a pure slope factorisation is nonzero.

theorem Polynomial.IsPureSlopeFactorization.newtonPolygon_ne_top {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) (m : ℝ) : (g m).newtonPolygon v ≠ ⊤

Every factor g m of a pure slope factorisation has a nonempty Newton polygon.

theorem Polynomial.IsPureSlopeFactorization.dvd {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) (m : ℝ) : g m ∣ f

Every factor g m divides f.

theorem Polynomial.IsPureSlopeFactorization.one {R : Type u_1} [CommRing R] (v : AddValuation R (WithTop ℝ)) : IsPureSlopeFactorization 1 v 1

The constant family 1 is a pure slope factorisation of 1.

theorem Polynomial.IsPureSlopeFactorization.of_forall_mem_newtonSlopes_eq {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} (hf0 : f.coeff 0 = 1) {m₀ : ℝ} (hm : ∀ s ∈ f.newtonSlopes v, s = m₀) : f.IsPureSlopeFactorization v (Function.update 1 m₀ f)

A constant-one polynomial pure of slope m₀ has pure slope factorisation Function.update 1 m₀ f.

theorem Polynomial.IsPureSlopeFactorization.mul {R : Type u_1} [CommRing R] {f₁ f₂ : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g₁ g₂ : ℝ → Polynomial R} (hg₁ : f₁.IsPureSlopeFactorization v g₁) (hg₂ : f₂.IsPureSlopeFactorization v g₂) : (f₁ * f₂).IsPureSlopeFactorization v (g₁ * g₂)

Pointwise multiplication of pure slope factorisations gives a pure slope factorisation of the product.

theorem Polynomial.IsPureSlopeFactorization.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hg : f.IsPureSlopeFactorization v g) (φ : R →+* S) {w : AddValuation S (WithTop ℝ)} (hφ : ∀ (x : R), w (φ x) = v x) : (Polynomial.map φ f).IsPureSlopeFactorization w fun (m : ℝ) => Polynomial.map φ (g m)

A pure slope factorisation is preserved by a ring homomorphism compatible with the valuations.

theorem Polynomial.IsPureSlopeFactorization.newtonSlopes_apply {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hg : f.IsPureSlopeFactorization v g) (m : ℝ) : (g m).newtonSlopes v = Multiset.replicate (g m).natDegree m

Each factor g m has finite slope multiset Multiset.replicate (g m).natDegree m.

theorem Polynomial.IsPureSlopeFactorization.natDegree_apply {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hg : f.IsPureSlopeFactorization v g) (m : ℝ) : (g m).natDegree = Multiset.count m (f.newtonSlopes v)

The degree of the slope-m factor is the multiplicity of m in f.newtonSlopes v.

theorem Polynomial.IsPureSlopeFactorization.apply_eq_one_iff {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hg : f.IsPureSlopeFactorization v g) {m : ℝ} : g m = 1 ↔ m ∉ f.newtonSlopes v

Outside the finite slopes of f, the factor g m is 1.

theorem Polynomial.IsPureSlopeFactorization.mulSupport_eq {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hg : f.IsPureSlopeFactorization v g) : Function.mulSupport g = {m : ℝ | m ∈ f.newtonSlopes v}

The multiplicative support of g is the set of finite Newton slopes of f.

theorem Polynomial.IsPureSlopeFactorization.prod_toFinset_eq {R : Type u_1} [CommRing R] {f : Polynomial R} {v : AddValuation R (WithTop ℝ)} {g : ℝ → Polynomial R} (hv : ∀ (x : R), v x = ⊤ → x = 0) (hg : f.IsPureSlopeFactorization v g) : ∏ m ∈ (f.newtonSlopes v).toFinset, g m = f

The product of g over the finset of distinct finite Newton slopes of f equals f.

theorem Polynomial.IsPureSlopeFactorization.pairwise_isCoprime {K : Type u_1} [Field K] {f : Polynomial K} {v : AddValuation K (WithTop ℝ)} {g : ℝ → Polynomial K} (hg : f.IsPureSlopeFactorization v g) : Pairwise fun (m₁ m₂ : ℝ) => IsCoprime (g m₁) (g m₂)

Distinct factors of a pure slope factorisation over a field are coprime.

theorem Polynomial.IsPureSlopeFactorization.unique {K : Type u_1} [Field K] {f : Polynomial K} {v : AddValuation K (WithTop ℝ)} {g₁ g₂ : ℝ → Polynomial K} (hg₁ : f.IsPureSlopeFactorization v g₁) (hg₂ : f.IsPureSlopeFactorization v g₂) : g₁ = g₂

Over a field, a polynomial has at most one pure slope factorisation.

@[simp]

theorem Polynomial.isPureSlopeFactorization_one_iff {K : Type u_1} [Field K] {v : AddValuation K (WithTop ℝ)} {g : ℝ → Polynomial K} : IsPureSlopeFactorization 1 v g ↔ g = 1

Over a field, only the constant family 1 is a pure slope factorisation of 1.

Existence of pure slope factorisations

theorem Polynomial.exists_mul_newtonSlopes_filter_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf0 : f.coeff 0 = 1) (σ : ℝ) : ∃ (P : Polynomial K) (Q : Polynomial K), P.coeff 0 = 1 ∧ Q.coeff 0 = 1 ∧ IsCoprime P Q ∧ P * Q = f ∧ P.newtonSlopes v = Multiset.filter (fun (x : ℝ) => x ≤ σ) (f.newtonSlopes v) ∧ Q.newtonSlopes v = Multiset.filter (fun (x : ℝ) => σ < x) (f.newtonSlopes v)

Threshold slope factorisation. Over a complete ultrametric normed field, any polynomial f with f.coeff 0 = 1 factors at any real threshold σ as f = P * Q, where P and Q are coprime constant-one polynomials carrying respectively the finite slopes ≤ σ and > σ of f.

theorem Polynomial.exists_isPureSlopeFactorization {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf0 : f.coeff 0 = 1) : ∃ (g : ℝ → Polynomial K), f.IsPureSlopeFactorization v g

Existence of the pure slope factorisation. Over a complete ultrametric normed field, every polynomial f with f.coeff 0 = 1 admits a pure slope factorisation over K.

theorem Polynomial.existsUnique_isPureSlopeFactorization {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf0 : f.coeff 0 = 1) : ∃! g : ℝ → Polynomial K, f.IsPureSlopeFactorization v g

Unique existence of the pure slope factorisation. Over a complete ultrametric normed field, every polynomial f with f.coeff 0 = 1 has a unique pure slope factorisation over K.

theorem Polynomial.existsUnique_C_mul_finprod_eq {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf0 : f.coeff 0 ≠ 0) : ∃! g : ℝ → Polynomial K, (Function.mulSupport g).Finite ∧ (∀ (m : ℝ), (g m).coeff 0 = 1) ∧ (∀ (m s : ℝ), s ∈ (g m).newtonSlopes v → s = m) ∧ C (f.coeff 0) * ∏ᶠ (m : ℝ), g m = f

Over a complete ultrametric normed field, any polynomial f with nonzero constant coefficient factors uniquely as C (f.coeff 0) * ∏ᶠ m, g m, where g is a family of constant-one pure factors.

theorem Polynomial.existsUnique_C_mul_X_pow_mul_finprod_eq {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf : f ≠ 0) : ∃! g : ℝ → Polynomial K, (Function.mulSupport g).Finite ∧ (∀ (m : ℝ), (g m).coeff 0 = 1) ∧ (∀ (m s : ℝ), s ∈ (g m).newtonSlopes v → s = m) ∧ C f.trailingCoeff * X ^ f.natTrailingDegree * ∏ᶠ (m : ℝ), g m = f

Over a complete ultrametric normed field, any nonzero polynomial f factors uniquely as C f.trailingCoeff * X ^ f.natTrailingDegree * ∏ᶠ m, g m, where g is a family of constant-one pure factors.

theorem Polynomial.splits_of_nodup_newtonSlopes {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] (v : AddValuation K (WithTop ℝ)) {b : ℝ} (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) {f : Polynomial K} (hf : (f.newtonSlopes v).Nodup) : f.Splits

Distinct-slopes splitting theorem. Over a complete ultrametric normed field, any polynomial whose finite Newton slopes have multiplicity one splits into linear factors over the base field.

Closed-disc pure slope factorisation of restricted power series

theorem PowerSeries.existsUnique_isUnit_X_pow_mul_finprod_eq {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₀)) [CompleteSpace K] {f : PowerSeries K} {σ : ℝ} (hfr : IsRestricted (b ^ σ) f) (hf0 : f ≠ 0) : ∃! p : ↥(IsRestricted.subring (b ^ σ)) × ℕ × (ℝ → Polynomial K), IsUnit p.1 ∧ (Function.mulSupport p.2.2).Finite ∧ (∀ (m : ℝ), (p.2.2 m).coeff 0 = 1) ∧ (∀ (m s : ℝ), s ∈ (p.2.2 m).newtonSlopes v → s = m) ∧ (∀ m ∈ Function.mulSupport p.2.2, m ≤ σ) ∧ ↑p.1 * ↑(Polynomial.X ^ p.2.1 * ∏ᶠ (m : ℝ), p.2.2 m) = f

Closed-disc pure slope factorisation of a restricted power series. Over a complete ultrametric normed field K, any nonzero power series f restricted at the radius b ^ σ factors uniquely as f = u * (X ^ a * ∏ᶠ m, g m), where u is a unit of the ring of series restricted at b ^ σ, a : ℕ is the order of vanishing of f at zero (PowerSeries.order_eq_of_isUnit_X_pow_mul_finprod_eq), and g : ℝ → K[X] is a finitely supported family of constant-one pure polynomials of slopes m ≤ σ.

theorem PowerSeries.existsUnique_isUnit_X_pow_mul_finprod_eq_of_pos {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₀)) [CompleteSpace K] {f : PowerSeries K} {r : ℝ} (hr : 0 < r) (hfr : IsRestricted r f) (hf0 : f ≠ 0) : ∃! p : ↥(IsRestricted.subring r) × ℕ × (ℝ → Polynomial K), IsUnit p.1 ∧ (Function.mulSupport p.2.2).Finite ∧ (∀ (m : ℝ), (p.2.2 m).coeff 0 = 1) ∧ (∀ (m s : ℝ), s ∈ (p.2.2 m).newtonSlopes v → s = m) ∧ (∀ m ∈ Function.mulSupport p.2.2, m ≤ Real.logb b r) ∧ ↑p.1 * ↑(Polynomial.X ^ p.2.1 * ∏ᶠ (m : ℝ), p.2.2 m) = f

Closed-disc pure slope factorisation at an arbitrary positive radius. For any r > 0, a nonzero power series f restricted at r factors uniquely into a unit at radius r, X ^ a, and constant-one pure polynomial factors of slopes m ≤ Real.logb b r.

theorem PowerSeries.setOf_norm_eq_and_evalAt_eq_zero {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₀)) {L : Type u_2} [NormedField L] [NormedAlgebra K L] [CompleteSpace L] {f : PowerSeries K} {r : ℝ} {u : ↥(IsRestricted.subring r)} (hu : IsUnit u) {a : ℕ} {g : ℝ → Polynomial K} (hfin : (Function.mulSupport g).Finite) (hc0 : ∀ (m : ℝ), (g m).coeff 0 = 1) (hslopes : ∀ (m s : ℝ), s ∈ (g m).newtonSlopes v → s = m) (hmul : ↑u * ↑(Polynomial.X ^ a * ∏ᶠ (m : ℝ), g m) = f) {m : ℝ} (hmr : b ^ m ≤ r) : {x : L | ‖x‖ = b ^ m ∧ f.evalAt x = 0} = {x : L | (Polynomial.aeval x) (g m) = 0}

Sphere decomposition of zeros on a closed disc. Under the hypotheses of PowerSeries.evalAt_eq_zero_iff_of_isUnit_X_pow_mul_finprod_eq with constant-one pure factors g m, for every slope m with b ^ m ≤ r the zeros of f on the sphere ‖x‖ = b ^ m in L are precisely the roots of the slope-m factor g m in L.