Puiseux's theorem

This file proves Puiseux's theorem: over an algebraically closed field K of characteristic zero, the field PuiseuxSeries K = ⋃ n, K((t ^ (1 / n))) of Puiseux series is algebraically closed, and is an algebraic closure of the Laurent series field K((t)).

The proof is the classical Newton–Puiseux algorithm, organized as a strong induction on the degree. Given a monic polynomial p of degree m over K((t)):

• a Tschirnhausen substitution X ↦ X + c kills the coefficient of degree m - 1 (this is where characteristic zero enters);
• if all lower coefficients vanish the polynomial is X ^ m, with root 0;
• otherwise, rescaling the variable by a monomial t ^ (a / (nq)) chosen by the minimal Newton slope produces a monic polynomial P over K⟦t⟧ whose reduction mod t is not a pure power (LaurentSeries.newton_slope_scaling);
• the reduction of P has a root of multiplicity strictly between 0 and m, so the Hensel splitting Polynomial.Monic.exists_factorization_rootMultiplicity produces a proper monic factor, and the induction hypothesis applies to it at a finer index (LaurentSeries.newton_puiseux_descent).

Main results

• PuiseuxSeries.exists_root_mem_subfield: every monic polynomial of positive degree over K((t)), mapped along any embedding LaurentSeries.toHahn K n, has a root in the Puiseux subfield of HahnSeries ℚ K.
• PuiseuxSeries.isAlgClosed: PuiseuxSeries K is algebraically closed for K algebraically closed of characteristic zero.
• PuiseuxSeries.isAlgClosure: Puiseux's theorem — PuiseuxSeries K is an algebraic closure of LaurentSeries K.

References

• [D. Eisenbud, Commutative Algebra with a view toward Algebraic Geometry][Eisenbud1995], Corollary 13.15

Tags

puiseux series, newton polygon, algebraically closed, algebraic closure

Auxiliary polynomial lemmas

Two generic lemmas over a field: the Tschirnhausen substitution killing the subleading coefficient, and the existence of a root of intermediate multiplicity for a monic polynomial with vanishing subleading coefficient which is not a pure power of X.

theorem Polynomial.Monic.tschirnhausen {F : Type u_1} [Field F] {p : Polynomial F} {m : ℕ} (hp : p.Monic) (hm : p.natDegree = m) (hmF : ↑m ≠ 0) : (p.comp (X + C (-p.coeff (m - 1) / ↑m))).Monic ∧ (p.comp (X + C (-p.coeff (m - 1) / ↑m))).natDegree = m ∧ (p.comp (X + C (-p.coeff (m - 1) / ↑m))).coeff (m - 1) = 0

Tschirnhausen substitution: for p monic of degree m over a field F with (m : F) ≠ 0, substituting X + C (-p.coeff (m - 1) / m) for the variable preserves monicity and degree and kills the coefficient of degree m - 1.

theorem Polynomial.Monic.exists_rootMultiplicity_pos_lt {K : Type u_1} [Field K] [IsAlgClosed K] {r : Polynomial K} {m : ℕ} (hr : r.Monic) (hm : r.natDegree = m) (hmK : ↑m ≠ 0) (hsub : r.coeff (m - 1) = 0) (hne : r ≠ X ^ m) : ∃ (a : K), 0 < rootMultiplicity a r ∧ rootMultiplicity a r < m

A monic non-power has a mixed root: over an algebraically closed field, a monic r of degree m with (m : K) ≠ 0, vanishing coefficient of degree m - 1, and r ≠ X ^ m has a root of multiplicity strictly between 0 and m.

The Newton slope rescaling

A Laurent series of nonnegative order is a power series; the per-summand monomial scaling identity for the embeddings toHahn; and the main rescaling lemma producing an integral polynomial with the right reduction and the root-transfer eval identity.

theorem LaurentSeries.exists_ofPowerSeries_eq_of_order_nonneg {K : Type u_1} [Field K] {f : LaurentSeries K} (hf : f = 0 ∨ 0 ≤ HahnSeries.order f) : ∃ (F : PowerSeries K), (HahnSeries.ofPowerSeries ℤ K) F = f

A Laurent series that is zero or has nonnegative order lies in the range of the coercion from power series.

theorem LaurentSeries.orderTop_expand {K : Type u_1} [Field K] (q : ℕ+) (c : LaurentSeries K) : HahnSeries.orderTop ((expand K q) c) = WithTop.map (fun (k : ℤ) => ↑↑q * k) (HahnSeries.orderTop c)

The expansion expand K q multiplies orderTop by q.

theorem LaurentSeries.toHahn_expand_single_scaling {K : Type u_1} [Field K] (n q : ℕ+) (a : ℤ) (c : LaurentSeries K) (i m : ℕ) : (HahnSeries.single (↑a / ↑↑(n * q))) 1 ^ m * (toHahn K (n * q)) ((expand K q) c * (HahnSeries.single (a * (↑i - ↑m))) 1) = (toHahn K n) c * (HahnSeries.single (↑a / ↑↑(n * q))) 1 ^ i

Monomial scaling identity (per-summand computation of the Newton rescaling): for τ = single (a / (nq)) 1, τ ^ m * toHahn K (n * q) (expand K q c * single (a * (i - m)) 1) = toHahn K n c * τ ^ i.

theorem LaurentSeries.newton_slope_scaling {K : Type u_1} [Field K] (n : ℕ+) {p : Polynomial (LaurentSeries K)} {m : ℕ} (hp : p.Monic) (hm : p.natDegree = m) (hsub : p.coeff (m - 1) = 0) (hex : ∃ i < m, p.coeff i ≠ 0) : ∃ (q : ℕ+) (a : ℤ) (P : Polynomial (PowerSeries K)), P.Monic ∧ P.natDegree = m ∧ (Polynomial.map PowerSeries.constantCoeff P).coeff (m - 1) = 0 ∧ (∃ i₀ < m, (Polynomial.map PowerSeries.constantCoeff P).coeff i₀ ≠ 0) ∧ ∀ (y : HahnSeries ℚ K), Polynomial.eval ((HahnSeries.single (↑a / ↑↑(n * q))) 1 * y) (Polynomial.map (toHahn K n) p) = (HahnSeries.single (↑a / ↑↑(n * q))) 1 ^ m * Polynomial.eval y (Polynomial.map ((toHahn K (n * q)).comp (HahnSeries.ofPowerSeries ℤ K)) P)

Newton slope scaling: given p monic of degree m over K((t)) with vanishing subleading coefficient and some nonzero lower coefficient, there are q ≥ 1, a : ℤ, and a monic P of degree m over K⟦X⟧ whose reduction has vanishing subleading coefficient but some nonzero coefficient below the top, such that roots transfer: evaluating p.map (toHahn K n) at τ * y (with τ = single (a / (nq)) 1) equals τ ^ m times the evaluation at y of the image of P under toHahn K (n * q) composed with the Laurent coercion.

The descent step and the main induction

theorem LaurentSeries.newton_puiseux_descent {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] (n : ℕ+) {p' : Polynomial (LaurentSeries K)} {m : ℕ} (hp : p'.Monic) (hm : p'.natDegree = m) (hsub : p'.coeff (m - 1) = 0) (hex : ∃ i < m, p'.coeff i ≠ 0) : ∃ (q : ℕ+) (τ : HahnSeries ℚ K) (g : Polynomial (LaurentSeries K)), τ ∈ (toHahn K (n * q)).fieldRange ∧ g.Monic ∧ 1 ≤ g.natDegree ∧ g.natDegree < m ∧ ∀ (y : HahnSeries ℚ K), Polynomial.eval y (Polynomial.map (toHahn K (n * q)) g) = 0 → Polynomial.eval (τ * y) (Polynomial.map (toHahn K n) p') = 0

Newton–Puiseux descent: for p' monic of degree m over K((t)) with vanishing subleading coefficient and some nonzero lower coefficient (K algebraically closed, characteristic zero), there are q ≥ 1, an element τ in the range of toHahn K (n * q), and a monic g with 1 ≤ deg g < m such that every root y of g.map (toHahn K (n * q)) gives the root τ * y of p'.map (toHahn K n).

theorem PuiseuxSeries.exists_root_mem_subfield {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] (n : ℕ+) {p : Polynomial (LaurentSeries K)} (hp : p.Monic) (hdeg : 1 ≤ p.natDegree) : ∃ x ∈ subfield K, Polynomial.eval x (Polynomial.map (LaurentSeries.toHahn K n) p) = 0

Puiseux root of a monic polynomial (the Newton–Puiseux induction): for K algebraically closed of characteristic zero, every monic p over K((t)) of positive degree, mapped along any embedding toHahn K n, has a root in the Puiseux subfield.

Main results

instance PuiseuxSeries.isAlgClosed (K : Type u_2) [Field K] [IsAlgClosed K] [CharZero K] : IsAlgClosed (PuiseuxSeries K)

Puiseux series are algebraically closed: for K an algebraically closed field of characteristic zero, the field of Puiseux series over K is algebraically closed. This is the analytic half of Puiseux's theorem, proved by the Newton–Puiseux algorithm.

instance PuiseuxSeries.isAlgClosure (K : Type u_2) [Field K] [IsAlgClosed K] [CharZero K] : IsAlgClosure (LaurentSeries K) (PuiseuxSeries K)

Puiseux's theorem: for K an algebraically closed field of characteristic zero, the Puiseux series field ⋃ n, K((t ^ (1 / n))) is an algebraic closure of the Laurent series field K((t)). Algebraicity holds over any field (PuiseuxSeries.isAlgebraic); algebraic closedness is the Newton–Puiseux algorithm (PuiseuxSeries.isAlgClosed).