The field of Puiseux series

This file defines the field of Puiseux series over a field K as a subfield of the Hahn series field HahnSeries ℚ K, namely the directed union of the images of the embeddings LaurentSeries.toHahn K n : K((t)) →+* HahnSeries ℚ K sending t to t ^ (1 / n).

Main definitions

• LaurentSeries.expand K m: the expansion ring endomorphism of K((t)) sending t to t ^ m.
• LaurentSeries.toHahn K n: the ring embedding K((t)) →+* HahnSeries ℚ K sending t to t ^ (1 / n).
• PuiseuxSeries.subfield K: the Puiseux subfield ⨆ n, (toHahn K n).fieldRange of HahnSeries ℚ K.
• PuiseuxSeries K: the type of Puiseux series over K, a field, equipped with an algebra structure over LaurentSeries K via toHahn K 1.

Main results

• PuiseuxSeries.mem_subfield_iff: membership in the Puiseux subfield is membership in the range of some toHahn K n.
• PuiseuxSeries.mem_subfield_iff_support: the classical bounded-denominator characterization — a Hahn series is a Puiseux series iff its support lies in (1 / n) • ℤ for a single n.
• PuiseuxSeries.exists_common_index: finitely many Puiseux series lie in the range of a single toHahn K N.

Tags

puiseux series, laurent series, hahn series

@[simp]

theorem HahnSeries.embDomain_embDomain {Γ : Type u_1} {Γ' : Type u_2} {Γ'' : Type u_3} {R : Type u_4} [PartialOrder Γ] [PartialOrder Γ'] [PartialOrder Γ''] [Zero R] (f : Γ ↪o Γ') (g : Γ' ↪o Γ'') (x : HahnSeries Γ R) : embDomain g (embDomain f x) = embDomain (RelEmbedding.trans f g) x

embDomain composes: extending along f and then along g is extending along f.trans g.

noncomputable def LaurentSeries.expand (K : Type u_1) [Field K] (m : ℕ+) : LaurentSeries K →+* LaurentSeries K

The expansion ring embedding K((t)) →+* K((t)), t ↦ t ^ m: embDomainRingHom along the exponent map k ↦ m * k on ℤ.

Equations

• LaurentSeries.expand K m = HahnSeries.embDomainRingHom (AddMonoidHom.mk' (fun (x : ℤ) => ↑↑m * x) ⋯) ⋯ ⋯

noncomputable def LaurentSeries.toHahn (K : Type u_1) [Field K] (n : ℕ+) : LaurentSeries K →+* HahnSeries ℚ K

The embedding K((t)) →+* HahnSeries ℚ K, "t ↦ t ^ (1 / n)": embDomainRingHom along the exponent map k ↦ k / n : ℤ → ℚ.

Equations

• LaurentSeries.toHahn K n = HahnSeries.embDomainRingHom (AddMonoidHom.mk' (fun (k : ℤ) => ↑k / ↑↑n) ⋯) ⋯ ⋯

@[simp]

theorem LaurentSeries.toHahn_single (K : Type u_1) [Field K] (n : ℕ+) (k : ℤ) (a : K) : (toHahn K n) ((HahnSeries.single k) a) = (HahnSeries.single (↑k / ↑↑n)) a

theorem LaurentSeries.toHahn_comp_expand (K : Type u_1) [Field K] (n m : ℕ+) : (toHahn K (n * m)).comp (expand K m) = toHahn K n

Compatibility of the embeddings: toHahn K n = toHahn K (n * m) ∘ expand K m — expanding by m and then mapping t ↦ t ^ (1 / (n * m)) is mapping t ↦ t ^ (1 / n).

theorem LaurentSeries.fieldRange_toHahn_le (K : Type u_1) [Field K] (n m : ℕ+) : (toHahn K n).fieldRange ≤ (toHahn K (n * m)).fieldRange

Range monotonicity: the range of toHahn K n is contained in the range of toHahn K (n * m), as subfields of HahnSeries ℚ K.

theorem LaurentSeries.directed_fieldRange_toHahn (K : Type u_1) [Field K] : Directed (fun (x1 x2 : Subfield (HahnSeries ℚ K)) => x1 ≤ x2) fun (n : ℕ+) => (toHahn K n).fieldRange

The family n ↦ (toHahn K n).fieldRange is directed: the ranges of toHahn K a and toHahn K b both sit inside the range of toHahn K (a * b).

noncomputable def PuiseuxSeries.subfield (K : Type u_1) [Field K] : Subfield (HahnSeries ℚ K)

The Puiseux subfield ⨆ n, (toHahn K n).fieldRange of HahnSeries ℚ K — the directed union of the images of the embeddings toHahn K n, i.e. ⋃ n, K((t ^ (1 / n))).

Equations

• PuiseuxSeries.subfield K = ⨆ (n : ℕ+), (LaurentSeries.toHahn K n).fieldRange

theorem PuiseuxSeries.mem_subfield_iff (K : Type u_1) [Field K] {x : HahnSeries ℚ K} : x ∈ subfield K ↔ ∃ (n : ℕ+), x ∈ (LaurentSeries.toHahn K n).fieldRange

Membership in the Puiseux subfield: x ∈ subfield K iff x is in the range of some toHahn K n (the supremum of the directed family of subfields is their union).

theorem PuiseuxSeries.mem_subfield_iff_support (K : Type u_1) [Field K] {x : HahnSeries ℚ K} : x ∈ subfield K ↔ ∃ (n : ℕ+), ∀ q ∈ x.support, ∃ (k : ℤ), q = ↑k / ↑↑n

Bounded-denominator characterization: membership in the Puiseux subfield is exactly the classical support condition — the support lies in (1 / n) • ℤ for a single n. This certifies the directed-union definition against the textbook description of Puiseux series.

theorem PuiseuxSeries.exists_common_index (K : Type u_1) [Field K] (s : Finset (HahnSeries ℚ K)) (hs : ∀ x ∈ s, x ∈ subfield K) : ∃ (N : ℕ+), ∀ x ∈ s, x ∈ (LaurentSeries.toHahn K N).fieldRange

Common index: a finite set of elements of the Puiseux subfield lies in the range of a single toHahn K N.

def PuiseuxSeries (K : Type u_1) [Field K] : Type u_1

The type of Puiseux series over K: the carrier of the Puiseux subfield of HahnSeries ℚ K. A field, by the generic subfield instances.

Equations

• PuiseuxSeries K = ↥(PuiseuxSeries.subfield K)

@[instance_reducible]

noncomputable instance PuiseuxSeries.instField (K : Type u_1) [Field K] : Field (PuiseuxSeries K)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance PuiseuxSeries.algebraLaurentSeries (K : Type u_1) [Field K] : Algebra (LaurentSeries K) (PuiseuxSeries K)

The K((t))-algebra structure on Puiseux series: toHahn K 1 corestricted to the Puiseux subfield. This fixes the embedding of K((t)) into the Puiseux series.

Equations

• PuiseuxSeries.algebraLaurentSeries K = ((LaurentSeries.toHahn K 1).codRestrict (PuiseuxSeries.subfield K) ⋯).toAlgebra