Depressed polynomials and their coprime splitting

A polynomial p of degree m over a field is depressed when its subleading coefficient p.nextCoeff vanishes. When m is invertible, the Tschirnhaus shift X ↦ X + r with r = -p.nextCoeff / (m * p.leadingCoeff) depresses p.

A monic depressed polynomial of invertible degree m that splits and is not X ^ m cannot be a power (X - a) ^ m of a single linear factor: for a ≠ 0 its subleading coefficient would be -m a ≠ 0, and for a = 0 it would be X ^ m. So it has a nonzero root a of multiplicity r with 0 < r < m, and p = (X - a) ^ r * q with q monic and coprime to (X - a) ^ r.

This is the factor-splitting input of the Newton–Puiseux algorithm: after normalization, the reduction modulo t of a monic depressed polynomial over K⟦t⟧ has this shape, and Hensel's lemma lifts the coprime splitting (Polynomial.Monic.exists_monic_mul_eq_of_nextCoeff_map_eq_zero in TauCeti.RingTheory.PowerSeries.Hensel).

Main results

• Polynomial.nextCoeff_taylor_neg_div_eq_zero: the Tschirnhaus shift depresses a polynomial whose degree is invertible.
• Polynomial.Monic.exists_isCoprime_mul_eq_of_nextCoeff_eq_zero: a monic depressed polynomial that splits, has invertible degree and is not a power of X is a product of two coprime monic factors of positive degree.

References

• H. Mannaa and T. Coquand, Dynamic Newton–Puiseux Theorem, arXiv:1304.6770, §1, for the centered polynomial and its coprime splitting in the Newton–Puiseux algorithm.

theorem Polynomial.nextCoeff_taylor_neg_div_eq_zero {K : Type u_1} [Field K] {p : Polynomial K} (hp : ↑p.natDegree ≠ 0) : ((taylor (-p.nextCoeff / (↑p.natDegree * p.leadingCoeff))) p).nextCoeff = 0

The Tschirnhaus shift: if the degree m of p is invertible, then p(X + r) with r = -p.nextCoeff / (m * p.leadingCoeff) has vanishing subleading coefficient.

theorem Polynomial.Monic.exists_isCoprime_mul_eq_of_nextCoeff_eq_zero {K : Type u_1} [Field K] {p : Polynomial K} (hp : p.Monic) (hs : p.Splits) (hm : ↑p.natDegree ≠ 0) (hnext : p.nextCoeff = 0) (hX : p ≠ X ^ p.natDegree) : ∃ (g : Polynomial K) (h : Polynomial K), g.Monic ∧ h.Monic ∧ IsCoprime g h ∧ g * h = p ∧ 0 < g.natDegree ∧ 0 < h.natDegree

A monic polynomial p with vanishing subleading coefficient that splits, whose degree is invertible, and which is not X ^ p.natDegree, factors as p = g * h with g and h monic, coprime and of positive degree.