The Puiseux field is an algebraic closure of the Laurent-series field

Let K be an algebraically closed field of characteristic zero. This file proves that the Puiseux field puiseuxField K is algebraically closed, and hence, being algebraic over K⸨X⸩, an algebraic closure of K⸨X⸩.

A polynomial P over the Puiseux field has its finitely many coefficients in a single ramified level n, so it is the image of a polynomial Q over K⸨u⸩ under the level-n embedding u ↦ t ^ (1 / n). The Newton–Puiseux theorem over K⸨u⸩ gives a root of Q after a further ramification u ↦ u ^ m, and the level-n * m embedding carries it to a root of P. In particular every root found this way lies in one ramified level.

Explicit roots of binomial equations over the Puiseux field are computed in TauCeti.RingTheory.LaurentSeries.Puiseux.Binomial.

Main results

• TauCeti.puiseuxField.exists_isRoot_levelEmbedding: a nonconstant polynomial over the Puiseux field has a root lying in a single ramified level.
• TauCeti.puiseuxField.instIsAlgClosed: the Puiseux field is algebraically closed.
• TauCeti.puiseuxField.instIsAlgClosure: the Puiseux field is an algebraic closure of K⸨X⸩.

References

• H. Mannaa and T. Coquand, Dynamic Newton–Puiseux Theorem, arXiv:1304.6770, §1.

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

Newton–Puiseux theorem. Over an algebraically closed field K of characteristic zero, every nonconstant polynomial over the Puiseux field has a root lying in a single ramified level.

instance TauCeti.puiseuxField.instIsAlgClosed {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] : IsAlgClosed ↥(puiseuxField K)

Over an algebraically closed field K of characteristic zero, the Puiseux field is algebraically closed.

instance TauCeti.puiseuxField.instIsAlgClosure {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] : IsAlgClosure (LaurentSeries K) ↥(puiseuxField K)

Over an algebraically closed field K of characteristic zero, the Puiseux field is an algebraic closure of the Laurent-series field K⸨X⸩.