Ramified levels of Laurent series

For a positive integer n, the Laurent series ring R⸨X⸩ in a variable u embeds into the Hahn series HahnSeries ℚ R with rational exponents by u ↦ t ^ (1 / n): the coefficient of u ^ k becomes the coefficient of t ^ (k / n). Its image, the level-n copy of R⸨X⸩, consists of the Hahn series all of whose exponents have denominator dividing n. For n ∣ m the levels are related by the substitution u_n ↦ u_m ^ (m / n), which is the exponent expansion X ↦ X ^ d of Laurent series. Over a field, the Puiseux series field is the union of these levels.

Both maps are HahnSeries.embDomain along an additive order embedding of exponent groups, k ↦ k / n from ℤ to ℚ and k ↦ d * k from ℤ to ℤ. They are algebra homomorphisms for the default R-algebra structures on R⸨X⸩ and HahnSeries ℚ R, those inherited from R⟦X⟧ through HahnSeries.powerSeriesAlgebra. Mathlib's HahnSeries.embDomainAlgHom is stated for the coefficientwise structure HahnSeries.instAlgebra instead, which is propositionally but not definitionally equal to it, so the algebra maps here are assembled from the ring-level embDomain lemmas.

Main definitions

• LaurentSeries.expand R d: the R-algebra map R⸨X⸩ → R⸨X⸩ substituting X ↦ X ^ d.
• LaurentSeries.contract: the exponent-congruence component of a Laurent series.
• LaurentSeries.ramifiedEmbedding R n: the R-algebra map R⸨X⸩ → HahnSeries ℚ R substituting X ↦ t ^ (1 / n).

Main results

• LaurentSeries.coeff_expand_mul, LaurentSeries.coeff_expand_of_not_dvd, LaurentSeries.coeff_expand_of_lt_mul_order: the coefficients of expand R d f.
• LaurentSeries.orderTop_expand, LaurentSeries.order_expand and LaurentSeries.leadingCoeff_expand: expansion multiplies the order by d and preserves the leading coefficient.
• LaurentSeries.mem_range_expand_iff: a Laurent series is in the image of X ↦ X ^ d exactly when all its exponents are divisible by d.
• LaurentSeries.expand_coe: expand extends PowerSeries.expand.
• LaurentSeries.valuation_expand: over a field, expansion X ↦ X ^ d raises the valuation to the d-th power.
• FiniteField.LaurentSeries.expand_card: over a finite field with q elements, the expansion X ↦ X ^ q of a Laurent series is its q-th power.
• LaurentSeries.sum_single_mul_expand_contract: reconstruction from congruence components.
• LaurentSeries.contract_eq_of_sum_eq: uniqueness of the congruence components.
• LaurentSeries.contract_expand_mul: contract d (expand d g * h) r = g * contract d h r.
• LaurentSeries.coeff_ramifiedEmbedding_intCast_div, LaurentSeries.coeff_ramifiedEmbedding_of_not_den_dvd: the coefficients of the level-n embedding.
• LaurentSeries.mem_range_ramifiedEmbedding_iff: the level-n image consists of the Hahn series whose exponents all have denominator dividing n.
• LaurentSeries.ramifiedEmbedding_comp_expand: for m = n * d, the transition map X ↦ X ^ d from level n to level m commutes with the embeddings.
• LaurentSeries.range_ramifiedEmbedding_le_iff: level n is contained in level m exactly when n ∣ m.
• LaurentSeries.range_ramifiedEmbedding_inf: the intersection of levels n and m is level gcd n m.

The signature LaurentSeries.expand (d : ℕ+) follows the one proposed for Mathlib in mathlib4 PR #42313.

Expansion X ↦ X ^ d

noncomputable def LaurentSeries.expand (R : Type u_1) [CommSemiring R] (d : ℕ+) : LaurentSeries R →ₐ[R] LaurentSeries R

The substitution X ↦ X ^ d in Laurent series, sending the coefficient of X ^ k to the coefficient of X ^ (d * k).

@[simp]

theorem LaurentSeries.coeff_expand_mul {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) (k : ℤ) : ((expand R d) f).coeff (↑↑d * k) = f.coeff k

The coefficient of X ^ (d * k) in expand R d f is the coefficient of X ^ k in f.

theorem LaurentSeries.coeff_expand_of_not_dvd {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) {k : ℤ} (hk : ¬↑↑d ∣ k) : ((expand R d) f).coeff k = 0

The coefficients of expand R d f at exponents not divisible by d vanish.

theorem LaurentSeries.coeff_expand_of_lt_mul_order {R : Type u_1} [CommSemiring R] (d : ℕ+) {f : LaurentSeries R} {k : ℤ} (hk : k < ↑↑d * HahnSeries.order f) : ((expand R d) f).coeff k = 0

The coefficients of expand R d f below d times the order of f vanish.

@[simp]

theorem LaurentSeries.expand_single {R : Type u_1} [CommSemiring R] (d : ℕ+) (k : ℤ) (r : R) : (expand R d) ((HahnSeries.single k) r) = (HahnSeries.single (↑↑d * k)) r

Expansion sends the monomial r X ^ k to r X ^ (d * k).

theorem LaurentSeries.support_expand {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) : HahnSeries.support ((expand R d) f) = (fun (k : ℤ) => ↑↑d * k) '' HahnSeries.support f

The support of expand R d f is the support of f multiplied by d.

@[simp]

theorem LaurentSeries.orderTop_expand {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) : HahnSeries.orderTop ((expand R d) f) = ↑d • HahnSeries.orderTop f

Expansion multiplies the order by d.

theorem LaurentSeries.expand_injective {R : Type u_1} [CommSemiring R] (d : ℕ+) : Function.Injective ⇑(expand R d)

Expansion is injective.

@[simp]

theorem LaurentSeries.order_expand {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) : HahnSeries.order ((expand R d) f) = ↑↑d * HahnSeries.order f

Expansion multiplies the order by d; the zero series has order zero on both sides.

@[simp]

theorem LaurentSeries.leadingCoeff_expand {R : Type u_1} [CommSemiring R] (d : ℕ+) (f : LaurentSeries R) : HahnSeries.leadingCoeff ((expand R d) f) = HahnSeries.leadingCoeff f

Expansion preserves the leading coefficient.

theorem LaurentSeries.mem_range_expand_iff {R : Type u_1} [CommSemiring R] (d : ℕ+) {f : LaurentSeries R} : f ∈ (expand R d).range ↔ ∀ k ∈ HahnSeries.support f, ↑↑d ∣ k

A Laurent series is in the image of X ↦ X ^ d exactly when all its exponents are divisible by d.

@[simp]

theorem LaurentSeries.expand_one (R : Type u_1) [CommSemiring R] : expand R 1 = AlgHom.id R (LaurentSeries R)

Expansion by 1 is the identity.

theorem LaurentSeries.expand_expand {R : Type u_1} [CommSemiring R] (d e : ℕ+) (f : LaurentSeries R) : (expand R d) ((expand R e) f) = (expand R (d * e)) f

Expanding by e and then by d is expanding by d * e.

theorem LaurentSeries.expand_coe {R : Type u_2} [CommRing R] (d : ℕ+) (f : PowerSeries R) : (expand R d) ((HahnSeries.ofPowerSeries ℤ R) f) = (HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.expand ↑d ⋯) f)

On power series, expansion of Laurent series is Mathlib's PowerSeries.expand.

@[simp]

theorem LaurentSeries.valuation_expand {K : Type u_2} [Field K] (d : ℕ+) (f : LaurentSeries K) : Valued.v ((expand K d) f) = Valued.v f ^ ↑d

Expansion X ↦ X ^ d raises the X-adic valuation of a Laurent series to the d-th power: it multiplies the order by d.

theorem FiniteField.LaurentSeries.expand_card {K : Type u_2} [Field K] [Fintype K] (d : ℕ+) (hd : ↑d = Fintype.card K) (f : LaurentSeries K) : (LaurentSeries.expand K d) f = f ^ Fintype.card K

Over a finite field with q elements, the expansion X ↦ X ^ q of a Laurent series is its q-th power. The modulus is given as a positive natural number d with d = q.

Contraction by exponent congruence classes

noncomputable def LaurentSeries.contract {S : Type u_2} [Zero S] (d : ℕ+) (f : LaurentSeries S) (r : Fin ↑d) : LaurentSeries S

The r-th exponent-congruence component of a Laurent series. Its coefficient at k is the coefficient of the original series at d * k + r.

@[simp]

theorem LaurentSeries.coeff_contract {S : Type u_2} [Zero S] (d : ℕ+) (f : LaurentSeries S) (r : Fin ↑d) (k : ℤ) : (contract d f r).coeff k = f.coeff (↑↑d * k + ↑↑r)

The coefficient formula for an exponent-congruence component.

theorem LaurentSeries.continuous_contract {K : Type u_2} [Field K] (d : ℕ+) (r : Fin ↑d) : Continuous fun (f : LaurentSeries K) => contract d f r

Extracting an exponent-congruence component is continuous for the valuation topology.

@[simp]

theorem LaurentSeries.contract_add {S : Type u_2} [AddMonoid S] (d : ℕ+) (f g : LaurentSeries S) (r : Fin ↑d) : contract d (f + g) r = contract d f r + contract d g r

Contraction is additive.

@[simp]

theorem LaurentSeries.contract_zero {S : Type u_2} [Zero S] (d : ℕ+) (r : Fin ↑d) : contract d 0 r = 0

Every congruence component of the zero series is zero.

@[simp]

theorem LaurentSeries.contract_smul {M : Type u_2} {S : Type u_3} [Zero S] [SMulZeroClass M S] (d : ℕ+) (c : M) (f : LaurentSeries S) (r : Fin ↑d) : contract d (c • f) r = c • contract d f r

Contraction commutes with scalar multiplication.

@[simp]

theorem LaurentSeries.contract_sum {ι : Type u_2} {S : Type u_3} [AddCommMonoid S] (d : ℕ+) (s : Finset ι) (f : ι → LaurentSeries S) (r : Fin ↑d) : contract d (∑ i ∈ s, f i) r = ∑ i ∈ s, contract d (f i) r

Contraction commutes with finite sums.

@[simp]

theorem LaurentSeries.contract_single {S : Type u_2} [Zero S] (d : ℕ+) (m : ℤ) (a : S) (r : Fin ↑d) : contract d ((HahnSeries.single m) a) r = if ↑↑d ∣ m - ↑↑r then (HahnSeries.single ((m - ↑↑r) / ↑↑d)) a else 0

The congruence components of a monomial: X ^ m contributes to component r exactly when m ≡ r modulo d, and then as the monomial of exponent (m - r) / d.

@[simp]

theorem LaurentSeries.contract_one {S : Type u_2} [Zero S] [One S] (d : ℕ+) (r : Fin ↑d) : contract d 1 r = if r = 0 then 1 else 0

The congruence components of 1 vanish except at residue zero.

theorem LaurentSeries.coeff_sum_single_mul_expand {A : Type u_2} [CommSemiring A] (d : ℕ+) (g : Fin ↑d → LaurentSeries A) (r : Fin ↑d) (k : ℤ) : (∑ s : Fin ↑d, (HahnSeries.single ↑↑s) 1 * (expand A d) (g s)).coeff (↑↑d * k + ↑↑r) = (g r).coeff k

At exponent d * k + r, a sum of expanded congruence components recovers coefficient k of component r.

theorem LaurentSeries.sum_single_mul_expand_contract {A : Type u_2} [CommSemiring A] (d : ℕ+) (f : LaurentSeries A) : ∑ r : Fin ↑d, (HahnSeries.single ↑↑r) 1 * (expand A d) (contract d f r) = f

A Laurent series is the sum of its expanded exponent-congruence components.

theorem LaurentSeries.contract_eq_of_sum_eq {A : Type u_2} [CommSemiring A] (d : ℕ+) (g : Fin ↑d → LaurentSeries A) (f : LaurentSeries A) (h : ∑ r : Fin ↑d, (HahnSeries.single ↑↑r) 1 * (expand A d) (g r) = f) (r : Fin ↑d) : contract d f r = g r

The components in an expansion by exponent congruence classes are unique.

@[simp]

theorem LaurentSeries.contract_expand_mul {A : Type u_2} [CommSemiring A] (d : ℕ+) (g h : LaurentSeries A) (r : Fin ↑d) : contract d ((expand A d) g * h) r = g * contract d h r

Multiplication by an expanded series passes through the exponent-congruence components.

@[simp]

theorem LaurentSeries.contract_expand {A : Type u_2} [CommSemiring A] (d : ℕ+) (g : LaurentSeries A) (r : Fin ↑d) : contract d ((expand A d) g) r = if r = 0 then g else 0

The congruence components of an expanded series: expand A d g lies in the residue-zero component, where it contracts back to g.

@[simp]

theorem LaurentSeries.contract_single_mul_self {A : Type u_2} [Semiring A] (d : ℕ+) (f : LaurentSeries A) (r : Fin ↑d) : contract d ((HahnSeries.single ↑↑r) 1 * f) r = contract d f 0

Multiplication by X ^ r, for r < d, moves the residue-zero component to component r.

Ramified levels in rational exponents

noncomputable def LaurentSeries.ramifiedEmbedding (R : Type u_1) [CommSemiring R] (n : ℕ+) : LaurentSeries R →ₐ[R] HahnSeries ℚ R

The level-n embedding of Laurent series into Hahn series with rational exponents, substituting X ↦ t ^ (1 / n): the coefficient of X ^ k becomes the coefficient of t ^ (k / n).

@[simp]

theorem LaurentSeries.coeff_ramifiedEmbedding_intCast_div {R : Type u_1} [CommSemiring R] (n : ℕ+) (f : LaurentSeries R) (k : ℤ) : ((ramifiedEmbedding R n) f).coeff (↑k / ↑↑n) = f.coeff k

The coefficient of t ^ (k / n) in the level-n image of f is the coefficient of X ^ k in f.

theorem LaurentSeries.coeff_ramifiedEmbedding_of_not_den_dvd {R : Type u_1} [CommSemiring R] (n : ℕ+) (f : LaurentSeries R) {q : ℚ} (hq : ¬q.den ∣ ↑n) : ((ramifiedEmbedding R n) f).coeff q = 0

The coefficients of the level-n image of f vanish at exponents whose denominator does not divide n.

@[simp]

theorem LaurentSeries.ramifiedEmbedding_single {R : Type u_1} [CommSemiring R] (n : ℕ+) (k : ℤ) (r : R) : (ramifiedEmbedding R n) ((HahnSeries.single k) r) = (HahnSeries.single (↑k / ↑↑n)) r

The level-n embedding sends the monomial r X ^ k to r t ^ (k / n).

theorem LaurentSeries.support_ramifiedEmbedding {R : Type u_1} [CommSemiring R] (n : ℕ+) (f : LaurentSeries R) : ((ramifiedEmbedding R n) f).support = (fun (k : ℤ) => ↑k / ↑↑n) '' HahnSeries.support f

The support of the level-n image of f is the support of f divided by n.

@[simp]

theorem LaurentSeries.orderTop_ramifiedEmbedding {R : Type u_1} [CommSemiring R] (n : ℕ+) (f : LaurentSeries R) : ((ramifiedEmbedding R n) f).orderTop = WithTop.map (fun (k : ℤ) => ↑k / ↑↑n) (HahnSeries.orderTop f)

The order of the level-n image of f is the order of f divided by n.

theorem LaurentSeries.ramifiedEmbedding_injective {R : Type u_1} [CommSemiring R] (n : ℕ+) : Function.Injective ⇑(ramifiedEmbedding R n)

The level-n embedding is injective.

@[simp]

theorem LaurentSeries.order_ramifiedEmbedding {R : Type u_1} [CommSemiring R] (n : ℕ+) (f : LaurentSeries R) : ((ramifiedEmbedding R n) f).order = ↑(HahnSeries.order f) / ↑↑n

The order of the level-n image of f is the order of f divided by n.

theorem LaurentSeries.mem_range_ramifiedEmbedding_iff {R : Type u_1} [CommSemiring R] (n : ℕ+) {x : HahnSeries ℚ R} : x ∈ (ramifiedEmbedding R n).range ↔ ∀ q ∈ x.support, q.den ∣ ↑n

The level-n image consists of the Hahn series all of whose exponents have denominator dividing n.

@[simp]

theorem LaurentSeries.ramifiedEmbedding_expand {R : Type u_1} [CommSemiring R] (n d : ℕ+) (f : LaurentSeries R) : (ramifiedEmbedding R (n * d)) ((expand R d) f) = (ramifiedEmbedding R n) f

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

theorem LaurentSeries.ramifiedEmbedding_comp_expand {R : Type u_1} [CommSemiring R] (n d : ℕ+) : (ramifiedEmbedding R (n * d)).comp (expand R d) = ramifiedEmbedding R n

ramifiedEmbedding_expand as an equality of algebra maps.

theorem LaurentSeries.range_ramifiedEmbedding_le_of_dvd {R : Type u_1} [CommSemiring R] {n m : ℕ+} (h : n ∣ m) : (ramifiedEmbedding R n).range ≤ (ramifiedEmbedding R m).range

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

theorem LaurentSeries.range_ramifiedEmbedding_le_iff {R : Type u_1} [CommSemiring R] [Nontrivial R] {n m : ℕ+} : (ramifiedEmbedding R n).range ≤ (ramifiedEmbedding R m).range ↔ n ∣ m

Over a nontrivial ring, level n is contained in level m exactly when n ∣ m.

theorem LaurentSeries.range_ramifiedEmbedding_inf {R : Type u_1} [CommSemiring R] (n m : ℕ+) : (ramifiedEmbedding R n).range ⊓ (ramifiedEmbedding R m).range = (ramifiedEmbedding R (n.gcd m)).range

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