Slope normalization of monic polynomials over Laurent series

Let P = Y ^ m + a₁ Y ^ (m - 1) + ⋯ + a_m be a monic polynomial over R⸨t⸩ other than Y ^ m. Among its nonzero lower coefficients a_i, i ≥ 1, choose one minimizing the slope ord(a_i) / i, and write that slope as p / q with q = i > 0. After the ramified substitution t = s ^ q, the rescaling Y = s ^ p Z and division by s ^ (p m), the polynomial becomes

Z ^ m + a₁(s ^ q) s ^ (-p) Z ^ (m - 1) + ⋯ + a_m(s ^ q) s ^ (-p m),

whose coefficients have order q ord(a_i) - p i ≥ 0, with equality at the chosen index. So it is a monic polynomial Q over R⟦s⟧ whose reduction modulo s has a nonzero coefficient below the leading one, that is, the reduction is not Z ^ m. Division by s ^ (p m) after Y = s ^ p Z is root scaling by s ^ p, so P(s ^ q, Y) is Polynomial.scaleRoots Q (s ^ p); a root z of Q gives the root s ^ p z of P(s ^ q, Y), and factorizations of Q transport to factorizations of P(s ^ q, Y) (Polynomial.scaleRoots_eval₂_mul, Polynomial.mul_scaleRoots'). Root scaling multiplies the subleading coefficient by a unit, so Q is depressed when P is.

This is the normalization step of the formal Newton–Puiseux theorem. When P is depressed, so is the reduction of Q; if that reduction moreover splits and its degree m is invertible, then it is not (Z - c) ^ m: its subleading coefficient -m c vanishes, forcing c = 0, and the reduction is not Z ^ m. So it has two distinct roots and factors into coprime monic factors, and Hensel's lemma lifts this to a factorization of Q into monic factors of lower degree.

Main results

• Polynomial.Monic.exists_map_expand_eq_scaleRoots: a monic polynomial P over R⸨X⸩ other than X ^ P.natDegree becomes, after a substitution X ↦ X ^ q in its coefficients, the root scaling by X ^ p of a monic polynomial over R⟦X⟧ of the same degree whose reduction is not a power of X.
• Polynomial.Monic.exists_map_expand_eq_scaleRoots_of_nextCoeff_eq_zero: if moreover P has vanishing subleading coefficient, then so does the reduction of the normalized polynomial.
• Polynomial.Monic.exists_coeff_ne_zero_slope_le: the choice of a nonzero lower coefficient of least slope, and Polynomial.coeff_scaleRoots_map_expand: the coefficients of the ramified and rescaled polynomial.

References

• H. Mannaa and T. Coquand, Dynamic Newton–Puiseux Theorem, arXiv:1304.6770, §1, for the ramification and rescaling step of the Newton–Puiseux algorithm.

theorem Polynomial.Monic.exists_coeff_ne_zero_slope_le {R : Type u_1} [Semiring R] {P : Polynomial (LaurentSeries R)} (hP : P.Monic) (hX : P ≠ X ^ P.natDegree) : ∃ j₀ < P.natDegree, P.coeff j₀ ≠ 0 ∧ ∀ (j : ℕ), P.coeff j ≠ 0 → ↑(P.natDegree - j) * HahnSeries.order (P.coeff j₀) ≤ ↑(P.natDegree - j₀) * HahnSeries.order (P.coeff j)

Least slope. A monic polynomial P over R⸨X⸩ other than X ^ P.natDegree has a nonzero coefficient a_{j₀}, j₀ < P.natDegree, of least slope: for every nonzero lower coefficient a_j, the inequality ord(a_{j₀}) / (P.natDegree - j₀) ≤ ord(a_j) / (P.natDegree - j) holds, stated with the denominators cleared.

theorem Polynomial.coeff_scaleRoots_map_expand {R : Type u_1} [CommSemiring R] (P : Polynomial (LaurentSeries R)) (q : ℕ+) (p : ℤ) (j : ℕ) : ((map (↑(LaurentSeries.expand R q)) P).scaleRoots ((HahnSeries.single (-p)) 1)).coeff j = (LaurentSeries.expand R q) (P.coeff j) * (HahnSeries.single (-(↑(P.natDegree - j) * p))) 1

The coefficients of P(X ^ q, X ^ p Y) / X ^ (p m), where m = P.natDegree: the root scaling by X ^ (-p) of P with the substitution X ↦ X ^ q applied to its coefficients.

theorem Polynomial.Monic.exists_map_expand_eq_scaleRoots {R : Type u_1} [CommSemiring R] {P : Polynomial (LaurentSeries R)} (hP : P.Monic) (hX : P ≠ X ^ P.natDegree) : ∃ (q : ℕ+) (p : ℤ) (Q : Polynomial (PowerSeries R)), Q.Monic ∧ Q.natDegree = P.natDegree ∧ Polynomial.map (↑(LaurentSeries.expand R q)) P = (Polynomial.map (HahnSeries.ofPowerSeries ℤ R) Q).scaleRoots ((HahnSeries.single p) 1) ∧ Polynomial.map PowerSeries.constantCoeff Q ≠ X ^ Q.natDegree

Slope normalization. A monic polynomial P over R⸨X⸩ other than X ^ P.natDegree becomes, after the ramified substitution X ↦ X ^ q in its coefficients, the root scaling by X ^ p of a monic polynomial Q over R⟦X⟧ of the same degree whose reduction modulo X is not X ^ Q.natDegree.

theorem Polynomial.Monic.exists_map_expand_eq_scaleRoots_of_nextCoeff_eq_zero {R : Type u_1} [CommSemiring R] {P : Polynomial (LaurentSeries R)} (hP : P.Monic) (hnext : P.nextCoeff = 0) (hX : P ≠ X ^ P.natDegree) : ∃ (q : ℕ+) (p : ℤ) (Q : Polynomial (PowerSeries R)), Q.Monic ∧ Q.natDegree = P.natDegree ∧ Polynomial.map (↑(LaurentSeries.expand R q)) P = (Polynomial.map (HahnSeries.ofPowerSeries ℤ R) Q).scaleRoots ((HahnSeries.single p) 1) ∧ (Polynomial.map PowerSeries.constantCoeff Q).nextCoeff = 0 ∧ Polynomial.map PowerSeries.constantCoeff Q ≠ X ^ Q.natDegree

Slope normalization of a depressed polynomial. If the monic polynomial P over R⸨X⸩ has vanishing subleading coefficient and is not X ^ P.natDegree, then it has a normalization Q as in Polynomial.Monic.exists_map_expand_eq_scaleRoots whose reduction modulo X also has vanishing subleading coefficient.