Puiseux series are algebraic over Laurent series

This file proves that the field of Puiseux series over a field K is algebraic over the field of Laurent series: the monomial t ^ (1 / n) is integral over the image of K((t)) (it is a root of the monic polynomial Y ^ n - t), and the image of toHahn K n lies in the subalgebra generated by this monomial (sorting a series in t ^ (1 / n) by exponent residues mod n).

Main results

• PuiseuxSeries.isIntegral_single_one_div: the monomial t ^ (1 / n) of HahnSeries ℚ K is integral over the range of LaurentSeries.toHahn K 1.
• PuiseuxSeries.mem_adjoin_single_of_mem_fieldRange: every element of the range of LaurentSeries.toHahn K n lies in the subalgebra generated by t ^ (1 / n) over the range of LaurentSeries.toHahn K 1.
• PuiseuxSeries.isAlgebraic: PuiseuxSeries K is algebraic over LaurentSeries K.

Tags

puiseux series, laurent series, algebraic

theorem PuiseuxSeries.isIntegral_single_one_div (K : Type u_1) [Field K] (n : ℕ+) : IsIntegral (↥(LaurentSeries.toHahn K 1).fieldRange) ((HahnSeries.single (1 / ↑↑n)) 1)

The monomial t ^ (1 / n) of HahnSeries ℚ K is integral over the range of LaurentSeries.toHahn K 1: it is a root of the monic polynomial Y ^ n - t.

theorem PuiseuxSeries.mem_adjoin_single_of_mem_fieldRange (K : Type u_1) [Field K] (n : ℕ+) {x : HahnSeries ℚ K} (hx : x ∈ (LaurentSeries.toHahn K n).fieldRange) : x ∈ (↥(LaurentSeries.toHahn K 1).fieldRange)[(HahnSeries.single (1 / ↑↑n)) 1]

Every element of the range of LaurentSeries.toHahn K n lies in the subalgebra of HahnSeries ℚ K generated by the monomial t ^ (1 / n) over the range of LaurentSeries.toHahn K 1 — sort a series in t ^ (1 / n) by exponent residues mod n.

instance PuiseuxSeries.isAlgebraic (K : Type u_1) [Field K] : Algebra.IsAlgebraic (LaurentSeries K) (PuiseuxSeries K)

Puiseux series are algebraic over Laurent series, for any field K.