Power bases of ramified Laurent-series levels

For a positive integer d, every Laurent series has a unique decomposition

f = ∑ r : Fin d, X ^ r * expand d (contract d f r).

Here contract d f r retains the coefficients of f in the congruence class r modulo d and sends each exponent d * k + r to k. This realizes the Laurent-series field in the variable u as a degree-d extension of the Laurent-series field in t = u ^ d, with power basis 1, u, ..., u ^ (d - 1).

The source and target fields have the same underlying Laurent-series type but different algebra structures. TauCeti.LaurentSeries.Level K d is therefore a wrapped copy of K⸨X⸩, with the base-field map given by LaurentSeries.expand K d. It embeds into the Puiseux field as its actual level-d subfield. Transporting the power basis proves that this subfield has degree d; since every Puiseux series lies in some level, the Puiseux field is algebraic over K⸨X⸩ in every characteristic.

The actual levels form a lattice of intermediate fields mirroring divisibility: level n lies in level m exactly when n ∣ m, the intersection of levels n and m is level gcd n m, their compositum is level lcm n m, level one is K⸨X⸩ and the levels exhaust the Puiseux field. These formulas reduce questions about finitely many ramified subextensions, such as the smallest level containing given Puiseux series, to divisibility of the levels.

The contraction and decomposition API follows the design proposed in Mathlib PR #42313.

Main definitions

• LaurentSeries.contract: the exponent-congruence component of a Laurent series.
• TauCeti.LaurentSeries.Level: the level-d Laurent field with base map X ↦ X ^ d.
• TauCeti.LaurentSeries.Level.powerBasis: the power basis 1, u, ..., u ^ (d - 1).
• TauCeti.puiseuxField.level: the actual level-d intermediate field in the Puiseux field.
• TauCeti.puiseuxField.levelPowerBasis: its transported power basis.

Main results

• LaurentSeries.sum_single_mul_expand_contract: reconstruction from congruence components.
• LaurentSeries.contract_eq_of_sum_eq: uniqueness of the congruence components.
• TauCeti.puiseuxField.level_finrank: level d has degree d over K⸨X⸩.
• TauCeti.puiseuxField.isAlgebraic_laurentSeries: every Puiseux series is algebraic over K⸨X⸩.
• TauCeti.puiseuxField.level_le_level_iff: level n lies in level m exactly when n ∣ m.
• TauCeti.puiseuxField.finrank_restrict_level: level n has degree n over K⸨X⸩ as an intermediate field of level m.
• TauCeti.puiseuxField.level_inf_level: levels n and m intersect in level gcd n m.
• TauCeti.puiseuxField.level_sup_level: levels n and m generate level lcm n m.
• TauCeti.puiseuxField.iSup_level: the levels exhaust the Puiseux field.
• IntermediateField.exists_le_level: a finite-dimensional intermediate field of the Puiseux field lies in a single level.

structure TauCeti.LaurentSeries.Level (K : Type u_1) [Field K] (d : ℕ+) : Type u_1

A wrapped copy of the Laurent-series field at ramified level d. Its field structure is the usual one, while its K⸨X⸩-algebra structure sends the base parameter to the d-th power of the level parameter. The wrapper avoids installing two algebra structures on K⸨X⸩ itself.

• ofLaurentSeries :: (
• toLaurentSeries : LaurentSeries K

  The Laurent series underlying an element of a ramified level.

• )

theorem TauCeti.LaurentSeries.Level.ext {K : Type u_1} {inst✝ : Field K} {d : ℕ+} {x y : Level K d} (toLaurentSeries : x.toLaurentSeries = y.toLaurentSeries) : x = y

theorem TauCeti.LaurentSeries.Level.ext_iff {K : Type u_1} {inst✝ : Field K} {d : ℕ+} {x y : Level K d} : x = y ↔ x.toLaurentSeries = y.toLaurentSeries

def TauCeti.LaurentSeries.Level.equivLaurentSeries (K : Type u_1) [Field K] (d : ℕ+) : Level K d ≃ LaurentSeries K

The underlying Laurent series of a ramified-level element.

@[instance_reducible]

noncomputable instance TauCeti.LaurentSeries.Level.instField (K : Type u_1) [Field K] (d : ℕ+) : Field (Level K d)

A ramified level has the field structure of its underlying Laurent series.

def TauCeti.LaurentSeries.Level.ringEquivLaurentSeries (K : Type u_1) [Field K] (d : ℕ+) : Level K d ≃+* LaurentSeries K

The ring equivalence from a ramified level to its underlying Laurent-series field.

noncomputable def TauCeti.LaurentSeries.Level.algebraMap (K : Type u_1) [Field K] (d : ℕ+) : LaurentSeries K →+* Level K d

The base-field map into level d, given on underlying Laurent series by expansion X ↦ X ^ d.

@[instance_reducible]

noncomputable instance TauCeti.LaurentSeries.Level.instAlgebraLaurentSeries (K : Type u_1) [Field K] (d : ℕ+) : Algebra (LaurentSeries K) (Level K d)

Level d is a K⸨X⸩-algebra through the expansion X ↦ X ^ d.

@[simp]

theorem TauCeti.LaurentSeries.Level.algebraMap_apply (K : Type u_1) [Field K] (d : ℕ+) (f : LaurentSeries K) : (ringEquivLaurentSeries K d) ((Algebra.algebraMap (LaurentSeries K) (Level K d)) f) = (LaurentSeries.expand K d) f

The algebra map into a ramified level is expansion on underlying Laurent series.

@[simp]

theorem TauCeti.LaurentSeries.Level.ringEquivLaurentSeries_ofLaurentSeries (K : Type u_1) [Field K] (d : ℕ+) (f : LaurentSeries K) : (ringEquivLaurentSeries K d) { toLaurentSeries := f } = f

Wrapping and then taking the underlying Laurent series is the identity.

noncomputable def TauCeti.LaurentSeries.Level.basis (K : Type u_2) [Field K] (d : ℕ+) : Module.Basis (Fin ↑d) (LaurentSeries K) (Level K d)

The basis of level d obtained by splitting exponents modulo d.

noncomputable def TauCeti.LaurentSeries.Level.parameter (K : Type u_2) [Field K] (d : ℕ+) : Level K d

The level parameter u, whose d-th power is the base parameter.

@[simp]

theorem TauCeti.LaurentSeries.Level.ringEquiv_parameter (K : Type u_2) [Field K] (d : ℕ+) : (ringEquivLaurentSeries K d) (parameter K d) = (HahnSeries.single 1) 1

The underlying Laurent series of the level parameter is X.

theorem TauCeti.LaurentSeries.Level.parameter_pow (K : Type u_2) [Field K] (d : ℕ+) : parameter K d ^ ↑d = (Algebra.algebraMap (LaurentSeries K) (Level K d)) ((HahnSeries.single 1) 1)

The level parameter is a d-th root of the base parameter.

@[simp]

theorem TauCeti.LaurentSeries.Level.basis_apply (K : Type u_2) [Field K] (d : ℕ+) (r : Fin ↑d) : (basis K d) r = parameter K d ^ ↑r

The basis vectors of level d are 1, u, ..., u ^ (d - 1).

@[simp]

theorem TauCeti.LaurentSeries.Level.basis_repr_apply (K : Type u_2) [Field K] (d : ℕ+) (f : Level K d) (r : Fin ↑d) : ((basis K d).repr f) r = LaurentSeries.contract d ((ringEquivLaurentSeries K d) f) r

The coordinates of a level element in the power basis are its exponent-congruence components.

noncomputable def TauCeti.LaurentSeries.Level.powerBasis (K : Type u_2) [Field K] (d : ℕ+) : PowerBasis (LaurentSeries K) (Level K d)

The power basis 1, u, ..., u ^ (d - 1) of the ramified Laurent-series level.

@[simp]

theorem TauCeti.LaurentSeries.Level.powerBasis_gen (K : Type u_2) [Field K] (d : ℕ+) : (powerBasis K d).gen = parameter K d

The generator of the level power basis is the level parameter.

@[simp]

theorem TauCeti.LaurentSeries.Level.powerBasis_dim (K : Type u_2) [Field K] (d : ℕ+) : (powerBasis K d).dim = ↑d

The dimension of the level power basis is d.

@[simp]

theorem TauCeti.LaurentSeries.Level.powerBasis_basis (K : Type u_2) [Field K] (d : ℕ+) : (powerBasis K d).basis.reindex (finCongr ⋯) = basis K d

The basis underlying the level power basis is the congruence-class basis.

instance TauCeti.LaurentSeries.Level.moduleFinite (K : Type u_2) [Field K] (d : ℕ+) : Module.Finite (LaurentSeries K) (Level K d)

A ramified Laurent-series level is finite-dimensional over the base Laurent field.

noncomputable def TauCeti.LaurentSeries.Level.toPuiseux (K : Type u_2) [Field K] (d : ℕ+) : Level K d →ₐ[LaurentSeries K] ↥(puiseuxField K)

The K⸨X⸩-algebra embedding of level d into the Puiseux field.

theorem TauCeti.LaurentSeries.Level.coe_toPuiseux (K : Type u_2) [Field K] (d : ℕ+) (f : Level K d) : ↑((toPuiseux K d) f) = (LaurentSeries.ramifiedEmbedding K d) ((ringEquivLaurentSeries K d) f)

As a rational-exponent Hahn series, the level embedding is the corresponding ramified embedding.

@[simp]

theorem TauCeti.LaurentSeries.Level.toPuiseux_apply (K : Type u_2) [Field K] (d : ℕ+) (f : Level K d) : (toPuiseux K d) f = (puiseuxField.levelEmbedding K d) ((ringEquivLaurentSeries K d) f)

The abstract level embedding agrees with puiseuxField.levelEmbedding on the underlying Laurent series.

noncomputable def TauCeti.puiseuxField.level (K : Type u_1) [Field K] (d : ℕ+) : IntermediateField (LaurentSeries K) ↥(puiseuxField K)

The actual level-d intermediate field inside the Puiseux field.

theorem TauCeti.puiseuxField.mem_level_iff (K : Type u_1) [Field K] (d : ℕ+) (x : ↥(puiseuxField K)) : x ∈ level K d ↔ x ∈ (levelEmbedding K d).range

Membership in the actual level is membership in the range of the corresponding level embedding.

noncomputable def TauCeti.puiseuxField.levelEquiv (K : Type u_1) [Field K] (d : ℕ+) : LaurentSeries.Level K d ≃ₐ[LaurentSeries K] ↥(level K d)

The abstract ramified Laurent-series level is equivalent to its image in the Puiseux field.

@[simp]

theorem TauCeti.puiseuxField.coe_levelEquiv_apply (K : Type u_1) [Field K] (d : ℕ+) (f : LaurentSeries.Level K d) : ↑((levelEquiv K d) f) = (LaurentSeries.Level.toPuiseux K d) f

The level equivalence is the level embedding after coercion to the Puiseux field.

noncomputable def TauCeti.puiseuxField.levelPowerBasis (K : Type u_1) [Field K] (d : ℕ+) : PowerBasis (LaurentSeries K) ↥(level K d)

The transported power basis of the actual level-d subfield of the Puiseux field.

@[simp]

theorem TauCeti.puiseuxField.levelPowerBasis_gen (K : Type u_1) [Field K] (d : ℕ+) : (levelPowerBasis K d).gen = (levelEquiv K d) (LaurentSeries.Level.parameter K d)

The generator of the actual level power basis is the image of the level parameter.

@[simp]

theorem TauCeti.puiseuxField.levelPowerBasis_dim (K : Type u_1) [Field K] (d : ℕ+) : (levelPowerBasis K d).dim = ↑d

The dimension of the actual level power basis is d.

@[simp]

theorem TauCeti.puiseuxField.levelPowerBasis_basis (K : Type u_1) [Field K] (d : ℕ+) : (levelPowerBasis K d).basis.reindex (finCongr ⋯) = (LaurentSeries.Level.basis K d).map ↑(levelEquiv K d)

The basis of the actual level is the transported congruence-class basis.

theorem TauCeti.puiseuxField.level_finrank (K : Type u_1) [Field K] (d : ℕ+) : Module.finrank (LaurentSeries K) ↥(level K d) = ↑d

The level-d Puiseux subfield has degree d over K⸨X⸩.

theorem TauCeti.puiseuxField.isAlgebraic_laurentSeries (K : Type u_1) [Field K] : Algebra.IsAlgebraic (LaurentSeries K) ↥(puiseuxField K)

The Puiseux field is algebraic over the Laurent-series field in every characteristic.

theorem TauCeti.puiseuxField.coe_levelPowerBasis_gen (K : Type u_1) [Field K] (d : ℕ+) : ↑↑(levelPowerBasis K d).gen = (HahnSeries.single (↑↑d)⁻¹) 1

The generator of the level-d power basis is the monomial t ^ (1 / d).

theorem TauCeti.puiseuxField.coe_levelPowerBasis_gen_pow (K : Type u_1) [Field K] {e L : ℕ+} {k : ℕ} (h : ↑L = ↑e * k) : ↑(levelPowerBasis K L).gen ^ k = ↑(levelPowerBasis K e).gen

The level parameters are compatible: if L = e * k, then (t ^ (1 / L)) ^ k = t ^ (1 / e).

theorem TauCeti.puiseuxField.levelPowerBasis_gen_ne_zero (K : Type u_1) [Field K] (d : ℕ+) : ↑(levelPowerBasis K d).gen ≠ 0

The generator t ^ (1 / d) of the level-d power basis is nonzero.

theorem TauCeti.puiseuxField.level_le_of_levelPowerBasis_gen_mem (K : Type u_1) [Field K] {d : ℕ+} {S : IntermediateField (LaurentSeries K) ↥(puiseuxField K)} (h : ↑(levelPowerBasis K d).gen ∈ S) : level K d ≤ S

An intermediate field containing the generator t ^ (1 / d) contains level d.

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

For n ∣ m, level n is contained in level m.

@[simp]

theorem TauCeti.puiseuxField.level_le_level_iff (K : Type u_1) [Field K] {n m : ℕ+} : level K n ≤ level K m ↔ n ∣ m

Level n is contained in level m exactly when n ∣ m.

theorem TauCeti.puiseuxField.finrank_restrict_level (K : Type u_1) [Field K] {n m : ℕ+} (h : n ∣ m) : Module.finrank (LaurentSeries K) ↥(IntermediateField.restrict ⋯) = ↑n

For n ∣ m, level n has degree n over K⸨X⸩, as an intermediate field of level m.

@[simp]

theorem TauCeti.puiseuxField.restrict_level_le_restrict_level_iff (K : Type u_1) [Field K] {n n' m : ℕ+} (h : n ∣ m) (h' : n' ∣ m) : IntermediateField.restrict ⋯ ≤ IntermediateField.restrict ⋯ ↔ n ∣ n'

For n ∣ m and n' ∣ m, level n is contained in level n', as intermediate fields of level m, exactly when n ∣ n'.

@[simp]

theorem TauCeti.puiseuxField.level_one (K : Type u_1) [Field K] : level K 1 = ⊥

Level one is the base field K⸨X⸩.

@[simp]

theorem TauCeti.puiseuxField.level_inf_level (K : Type u_1) [Field K] (n m : ℕ+) : level K n ⊓ level K m = level K (n.gcd m)

The intersection of levels n and m is level gcd n m.

@[simp]

theorem TauCeti.puiseuxField.level_sup_level (K : Type u_1) [Field K] (n m : ℕ+) : level K n ⊔ level K m = level K (n.lcm m)

The compositum of levels n and m is level lcm n m.

@[simp]

theorem TauCeti.puiseuxField.iSup_level (K : Type u_1) [Field K] : ⨆ (d : ℕ+), level K d = ⊤

The levels exhaust the Puiseux field.

theorem IntermediateField.exists_le_level {K : Type u_1} [Field K] (E : IntermediateField (LaurentSeries K) ↥(TauCeti.puiseuxField K)) [FiniteDimensional (LaurentSeries K) ↥E] : ∃ (n : ℕ+), E ≤ TauCeti.puiseuxField.level K n

A finite-dimensional intermediate field of the Puiseux field over K⸨X⸩ lies in a single ramified level.