The Puiseux series field

For a field K, the field of Puiseux series over K is the subfield of the rational-exponent Hahn series field HahnSeries ℚ K consisting of the series whose exponents have a common denominator: for some n > 0, every exponent in the support is of the form k / n with k ∈ ℤ. Equivalently, it is the union of the ramified levels K⸨t ^ (1 / n)⸩, the images of the embeddings LaurentSeries.ramifiedEmbedding K n : K⸨X⸩ → HahnSeries ℚ K, which form a directed system under divisibility of n.

This file constructs the Puiseux field as an intermediate field of HahnSeries ℚ K over K, proves that it is the union of the levels, and that any finite family of Puiseux series, in particular the coefficients of a polynomial, lies in a single common level. The Laurent series field K⸨X⸩ acts on it through the level-one embedding X ↦ t, and every level embedding is compatible with this action after the expansion X ↦ X ^ n. In characteristic zero with K algebraically closed the Puiseux field is an algebraic closure of K⸨X⸩ (the Newton–Puiseux theorem); the common-level lift of polynomial coefficients is what reduces root finding over the Puiseux field to a single level. Finally, the series ∑ j, t ^ ((j + 1) + 1 / (j + 2)), whose exponents have unbounded denominators, shows that the Puiseux field is a proper subfield of HahnSeries ℚ K.

Main definitions

• TauCeti.puiseuxField K: the Puiseux series field, as an IntermediateField K (HahnSeries ℚ K).
• TauCeti.puiseuxField.single K q a: the monomial a t ^ q as a Puiseux series.
• TauCeti.puiseuxField.levelEmbedding K n: the level-n embedding K⸨X⸩ →ₐ[K] puiseuxField K, X ↦ t ^ (1 / n).
• The K⸨X⸩-algebra structure on puiseuxField K given by levelEmbedding K 1, with IsScalarTower K K⸨X⸩ (puiseuxField K).

Main results

• TauCeti.mem_puiseuxField_iff: a Hahn series is a Puiseux series exactly when it lies in some level.
• TauCeti.mem_puiseuxField_iff_exists_den_dvd: a Hahn series is a Puiseux series exactly when the denominators of its exponents are bounded in divisibility by a single n.
• TauCeti.puiseuxField_eq_iSup_fieldRange: the Puiseux field is the supremum of the levels.
• TauCeti.puiseuxField.exists_forall_mem_range_levelEmbedding: a finite family of Puiseux series lies in a common level.
• TauCeti.puiseuxField.exists_map_levelEmbedding_eq: every polynomial over the Puiseux field is the image of a polynomial over K⸨X⸩ under a single level embedding.
• TauCeti.puiseuxField.levelEmbedding_expand_self: the level-n embedding restricted along X ↦ X ^ n is the K⸨X⸩-algebra map.
• TauCeti.puiseuxField_lt_top: the Puiseux field is a proper subfield of HahnSeries ℚ K.

noncomputable def TauCeti.puiseuxField (K : Type u_1) [Field K] : IntermediateField K (HahnSeries ℚ K)

The Puiseux series field over K: the Hahn series with rational exponents whose exponents have a common denominator, that is, the union of the ramified levels K⸨t ^ (1 / n)⸩.

theorem TauCeti.mem_puiseuxField_iff {K : Type u_1} [Field K] {x : HahnSeries ℚ K} : x ∈ puiseuxField K ↔ ∃ (n : ℕ+), x ∈ (LaurentSeries.ramifiedEmbedding K n).range

A Hahn series is a Puiseux series exactly when it lies in the level-n image K⸨t ^ (1 / n)⸩ for some n.

theorem TauCeti.mem_puiseuxField_iff_exists_den_dvd {K : Type u_1} [Field K] {x : HahnSeries ℚ K} : x ∈ puiseuxField K ↔ ∃ (n : ℕ+), ∀ q ∈ x.support, q.den ∣ ↑n

A Hahn series is a Puiseux series exactly when the denominators of all of its exponents divide a single positive integer n.

@[simp]

theorem TauCeti.ramifiedEmbedding_mem_puiseuxField {K : Type u_1} [Field K] (n : ℕ+) (f : LaurentSeries K) : (LaurentSeries.ramifiedEmbedding K n) f ∈ puiseuxField K

The level-n image of a Laurent series is a Puiseux series.

@[simp]

theorem TauCeti.single_mem_puiseuxField {K : Type u_1} [Field K] (q : ℚ) (a : K) : (HahnSeries.single q) a ∈ puiseuxField K

The monomial a t ^ q is a Puiseux series for every rational exponent q.

noncomputable def TauCeti.puiseuxField.single (K : Type u_1) [Field K] (q : ℚ) (a : K) : ↥(puiseuxField K)

The monomial a t ^ q as a Puiseux series.

@[simp]

theorem TauCeti.puiseuxField.coe_single {K : Type u_1} [Field K] (q : ℚ) (a : K) : ↑(single K q a) = (HahnSeries.single q) a

As a Hahn series, the monomial single K q a is HahnSeries.single q a.

@[simp]

theorem TauCeti.puiseuxField.single_eq_zero_iff {K : Type u_1} [Field K] {q : ℚ} {a : K} : single K q a = 0 ↔ a = 0

The monomial a t ^ q vanishes exactly when a = 0.

@[simp]

theorem TauCeti.puiseuxField.single_pow {K : Type u_1} [Field K] (q : ℚ) (a : K) (n : ℕ) : single K q a ^ n = single K (↑n * q) (a ^ n)

The n-th power of a monomial a t ^ q is the monomial a ^ n t ^ (n * q).

@[simp]

theorem TauCeti.puiseuxField.inv_single {K : Type u_1} [Field K] (q : ℚ) (a : K) : (single K q a)⁻¹ = single K (-q) a⁻¹

The inverse of a monomial a t ^ q is the monomial a⁻¹ t ^ (-q).

@[simp]

theorem TauCeti.puiseuxField.algebraMap_mul_single {K : Type u_1} [Field K] (c : K) (q : ℚ) (a : K) : (algebraMap K ↥(puiseuxField K)) c * single K q a = single K q (c * a)

Multiplying a monomial by a constant multiplies its coefficient.

theorem TauCeti.fieldRange_ramifiedEmbedding_le_puiseuxField {K : Type u_1} [Field K] (n : ℕ+) : (LaurentSeries.ramifiedEmbedding K n).fieldRange ≤ puiseuxField K

Each level K⸨t ^ (1 / n)⸩ is contained in the Puiseux field.

theorem TauCeti.directed_fieldRange_ramifiedEmbedding {K : Type u_1} [Field K] : Directed (fun (x1 x2 : IntermediateField K (HahnSeries ℚ K)) => x1 ≤ x2) fun (n : ℕ+) => (LaurentSeries.ramifiedEmbedding K n).fieldRange

The levels K⸨t ^ (1 / n)⸩ form a directed family of subfields under divisibility.

theorem TauCeti.puiseuxField_eq_iSup_fieldRange {K : Type u_1} [Field K] : puiseuxField K = ⨆ (n : ℕ+), (LaurentSeries.ramifiedEmbedding K n).fieldRange

The Puiseux field is the supremum of the levels K⸨t ^ (1 / n)⸩.

noncomputable def TauCeti.puiseuxField.levelEmbedding (K : Type u_1) [Field K] (n : ℕ+) : LaurentSeries K →ₐ[K] ↥(puiseuxField K)

The level-n embedding K⸨X⸩ → puiseuxField K, substituting X ↦ t ^ (1 / n).

@[simp]

theorem TauCeti.puiseuxField.coe_levelEmbedding {K : Type u_1} [Field K] (n : ℕ+) (f : LaurentSeries K) : ↑((levelEmbedding K n) f) = (LaurentSeries.ramifiedEmbedding K n) f

As a Hahn series, the level-n embedding of f is ramifiedEmbedding K n f.

theorem TauCeti.puiseuxField.levelEmbedding_single_self {K : Type u_1} [Field K] (n : ℕ+) : (levelEmbedding K n) ((HahnSeries.single ↑↑n) 1) = single K 1 1

The parameter t is the level-n image of u ^ n.

@[simp]

theorem TauCeti.puiseuxField.levelEmbedding_expand {K : Type u_1} [Field K] (n d : ℕ+) (f : LaurentSeries K) : (levelEmbedding K (n * d)) ((LaurentSeries.expand K d) f) = (levelEmbedding K n) f

The transition map X ↦ X ^ d from level n to level n * d commutes with the level embeddings into the Puiseux field.

@[simp]

theorem TauCeti.puiseuxField.levelEmbedding_expand_divExact {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) (f : LaurentSeries K) : (levelEmbedding K m) ((LaurentSeries.expand K (m.divExact n)) f) = (levelEmbedding K n) f

levelEmbedding_expand for a level m divisible by n: the transition map X ↦ X ^ (m / n) from level n to level m commutes with the level embeddings.

theorem TauCeti.puiseuxField.levelEmbedding_comp_expand {K : Type u_1} [Field K] (n d : ℕ+) : (levelEmbedding K (n * d)).comp (LaurentSeries.expand K d) = levelEmbedding K n

levelEmbedding_expand as an equality of algebra maps.

theorem TauCeti.puiseuxField.mem_range_levelEmbedding_iff {K : Type u_1} [Field K] {n : ℕ+} {x : ↥(puiseuxField K)} : x ∈ (levelEmbedding K n).range ↔ ↑x ∈ (LaurentSeries.ramifiedEmbedding K n).range

A Puiseux series lies in the image of the level-n embedding exactly when, as a Hahn series, it lies in the level-n image K⸨t ^ (1 / n)⸩.

theorem TauCeti.puiseuxField.exists_mem_range_levelEmbedding {K : Type u_1} [Field K] (x : ↥(puiseuxField K)) : ∃ (n : ℕ+), x ∈ (levelEmbedding K n).range

Every Puiseux series lies in some level.

theorem TauCeti.puiseuxField.range_levelEmbedding_le_of_dvd {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) : (levelEmbedding K n).range ≤ (levelEmbedding K m).range

For n ∣ m, the image of level n in the Puiseux field is contained in that of level m.

theorem TauCeti.puiseuxField.exists_forall_mem_range_levelEmbedding {K : Type u_1} [Field K] {ι : Type u_2} [Finite ι] (x : ι → ↥(puiseuxField K)) : ∃ (n : ℕ+), ∀ (i : ι), x i ∈ (levelEmbedding K n).range

Common level: a finite family of Puiseux series lies in a single level.

theorem TauCeti.puiseuxField.exists_map_levelEmbedding_eq {K : Type u_1} [Field K] (p : Polynomial ↥(puiseuxField K)) : ∃ (n : ℕ+) (q : Polynomial (LaurentSeries K)), Polynomial.map (↑(levelEmbedding K n)) q = p

Common-level lift of polynomial coefficients: every polynomial over the Puiseux field is the image of a polynomial over K⸨X⸩ under a single level embedding.

@[instance_reducible]

noncomputable instance TauCeti.puiseuxField.instAlgebraLaurentSeriesSubtypeHahnSeriesRatMemIntermediateField {K : Type u_1} [Field K] : Algebra (LaurentSeries K) ↥(puiseuxField K)

The Puiseux field is a K⸨X⸩-algebra through the level-one embedding X ↦ t.

theorem TauCeti.puiseuxField.algebraMap_laurentSeries_apply {K : Type u_1} [Field K] (f : LaurentSeries K) : (algebraMap (LaurentSeries K) ↥(puiseuxField K)) f = (levelEmbedding K 1) f

The K⸨X⸩-algebra map to the Puiseux field is the level-one embedding.

@[simp]

theorem TauCeti.puiseuxField.coe_algebraMap_laurentSeries {K : Type u_1} [Field K] (f : LaurentSeries K) : ↑((algebraMap (LaurentSeries K) ↥(puiseuxField K)) f) = (LaurentSeries.ramifiedEmbedding K 1) f

As a Hahn series, the image of f under the K⸨X⸩-algebra map is the level-one image ramifiedEmbedding K 1 f.

instance TauCeti.puiseuxField.instIsScalarTowerLaurentSeriesSubtypeHahnSeriesRatMemIntermediateField {K : Type u_1} [Field K] : IsScalarTower K (LaurentSeries K) ↥(puiseuxField K)

The K-algebra structure on the Puiseux field factors through the K⸨X⸩-algebra structure.

@[simp]

theorem TauCeti.puiseuxField.levelEmbedding_expand_self {K : Type u_1} [Field K] (n : ℕ+) (f : LaurentSeries K) : (levelEmbedding K n) ((LaurentSeries.expand K n) f) = (algebraMap (LaurentSeries K) ↥(puiseuxField K)) f

The level-n embedding restricted along the expansion X ↦ X ^ n is the K⸨X⸩-algebra map: as a subfield of the Puiseux field, level n contains K⸨X⸩ with X acting as t = (t ^ (1 / n)) ^ n.

A series with exponents of unbounded denominator

def TauCeti.puiseuxField.unboundedDenExponent (j : ℕ) : ℚ

The exponents (j + 1) + 1 / (j + 2) of the series ∑ j, t ^ ((j + 1) + 1 / (j + 2)), whose denominators j + 2 are unbounded.

theorem TauCeti.puiseuxField.strictMono_unboundedDenExponent : StrictMono unboundedDenExponent

The exponents (j + 1) + 1 / (j + 2) are strictly increasing.

theorem TauCeti.puiseuxField.tendsto_unboundedDenExponent : Filter.Tendsto unboundedDenExponent Filter.atTop Filter.atTop

The exponents (j + 1) + 1 / (j + 2) tend to infinity.

theorem TauCeti.puiseuxField.not_den_unboundedDenExponent_dvd (n : ℕ+) : ¬(unboundedDenExponent ↑n).den ∣ ↑n

The denominator n + 2 of the exponent (n + 1) + 1 / (n + 2) does not divide n.

theorem TauCeti.puiseuxField_lt_top (K : Type u_1) [Field K] : puiseuxField K < ⊤

The Puiseux field is a proper subfield of HahnSeries ℚ K: the rational Hahn series ∑ j, t ^ ((j + 1) + 1 / (j + 2)) has exponents of unbounded denominator.