The Newton–Puiseux theorem over a Laurent-series field

Let K be an algebraically closed field of characteristic zero. This file proves that every nonconstant polynomial P over K⸨X⸩ has a root after a finite ramification X ↦ X ^ n: there are n > 0 and y ∈ K⸨X⸩ with P(X ^ n)(y) = 0, where P(X ^ n) applies LaurentSeries.expand to the coefficients of P. Equivalently, P has a root in the level-n copy K⸨t ^ (1 / n)⸩ of the Puiseux series field.

The proof is the classical Newton–Puiseux algorithm, by induction on the degree m of P, which may be assumed monic.

1. Translating the variable by -a / m, where a is the coefficient of Y ^ (m - 1), removes that coefficient (Polynomial.nextCoeff_taylor_neg_div_eq_zero).
2. If the translated polynomial is Y ^ m, then 0 is a root. Otherwise choose the smallest slope ord (P.coeff j) / (m - j) over the nonzero coefficients with j < m, attained at j₀, and put q = m - j₀ and v = ord (P.coeff j₀). Ramifying X ↦ X ^ q and rescaling Y ↦ X ^ v * Y, then dividing by X ^ (v * m), produces a monic polynomial over K⟦X⟧ (Polynomial.Monic.exists_map_expand_eq_scaleRoots_of_nextCoeff_eq_zero). Its reduction modulo X still has no term of degree m - 1, and its coefficient of Y ^ j₀ is nonzero, so the reduction is not Y ^ m.
3. In characteristic zero such a reduction is not a power (Y - b) ^ m, so it splits into coprime monic factors of positive degree, and Hensel's lemma lifts this splitting to the rescaled polynomial (Polynomial.Monic.exists_monic_mul_eq_of_nextCoeff_map_eq_zero).
4. By induction the factor of degree r has a root after some ramification X ↦ X ^ n. Undoing the rescaling and the translation gives a root of P after the ramification X ↦ X ^ (n * q).

Through the level embeddings, the root theorem gives a root of P in the Puiseux field lying in a single ramified level. It is the input for the algebraic closedness of the Puiseux field.

Main results

• TauCeti.LaurentSeries.exists_isRoot_map_expand: a nonconstant polynomial over K⸨X⸩ has a root after a finite ramification X ↦ X ^ n.
• TauCeti.puiseuxField.exists_isRoot_map_levelEmbedding: a nonconstant polynomial over K⸨X⸩, embedded at any level, has a root in the Puiseux field lying in a single ramified level.

References

• H. Mannaa and T. Coquand, Dynamic Newton–Puiseux Theorem, arXiv:1304.6770, §1, for the proof by Tschirnhaus translation, ramification along the smallest slope, and Hensel splitting.

theorem TauCeti.LaurentSeries.exists_isRoot_map_expand {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {P : Polynomial (LaurentSeries K)} (hP : P.degree ≠ 0) : ∃ (n : ℕ+) (y : LaurentSeries K), (Polynomial.map (↑(LaurentSeries.expand K n)) P).IsRoot y

Newton–Puiseux theorem. Over an algebraically closed field K of characteristic zero, every nonconstant polynomial P over K⸨X⸩ has a root after a finite ramification: for some n > 0, the polynomial P(X ^ n) obtained by substituting X ↦ X ^ n in its coefficients has a root in K⸨X⸩.

theorem TauCeti.puiseuxField.exists_isRoot_map_levelEmbedding {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] (n : ℕ+) {P : Polynomial (LaurentSeries K)} (hP : P.degree ≠ 0) : ∃ (m : ℕ+) (y : LaurentSeries K), (Polynomial.map (↑(levelEmbedding K n)) P).IsRoot ((levelEmbedding K (n * m)) y)

Over an algebraically closed field K of characteristic zero, the image of a nonconstant polynomial over K⸨X⸩ under the level-n embedding X ↦ t ^ (1 / n) has a root in the Puiseux field lying in a single level n * m. For n = 1 the image is the polynomial over the Puiseux field obtained through the K⸨X⸩-algebra structure.