Laurent expansions and residues at rational places

Let P be a rational place of F / k and let t have order one at P. Passing to fraction fields, the identification of the completed valuation ring with k[[T]] becomes a k-algebra isomorphism of the completion of F at P with the Laurent-series field k((T)), sending t to T. It carries the valuation of P to the T-adic valuation.

Composing with the completion map gives the Laurent expansion of every function in F. Its coefficients below m depend only on the function modulo the m-th order filtration, and a finite sum ∑ cᵢ tⁱ congruent to the function modulo that filtration has exactly the coefficients cᵢ. The coefficient of T⁻¹ is the residue res_{P,t} of a function with respect to t. It vanishes on functions integral at P and is read off the power-series expansion of t ^ (n + 1) * z whenever this product is integral.

Main definitions

• TauCeti.Place.completionEquivLaurentSeries: the completion at a rational place is k((T)).
• TauCeti.Place.laurentSeriesExpansion: the Laurent expansion of functions at P in t.
• TauCeti.Place.residue: the residue res_{P,t}, the coefficient of t⁻¹.

Main results

• TauCeti.Place.valuation_completionEquivLaurentSeries: the isomorphism with k((T)) identifies the valuation of P with the T-adic valuation.
• TauCeti.Place.coeff_laurentSeriesExpansion_eq_of_sub_sum_mem_filtration: uniqueness of finite Laurent expansions.
• TauCeti.Place.mem_filtration_iff_forall_laurentCoeff_eq_zero: a function vanishes to order at least m exactly when its Laurent coefficients below m vanish; in particular the coefficient in the degree of the order is nonzero (TauCeti.Place.laurentCoeff_ord_ne_zero), the coefficients below the order vanish (TauCeti.Place.laurentCoeff_eq_zero_of_lt_ord), and a nonzero coefficient bounds the order (TauCeti.Place.ord_le_of_laurentCoeff_ne_zero).
• TauCeti.Place.sub_sum_laurentCoeff_mem_filtration: truncating the Laurent expansion below m leaves a function vanishing to order at least m.
• TauCeti.Place.residue_eq_coeff_powerSeriesExpansion: the residue as a power-series coefficient.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2, Definition 4.2.8.

Laurent expansions of functions

noncomputable def TauCeti.Place.laurentSeriesExpansion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : F →ₐ[k] LaurentSeries k

The Laurent expansion of a function at a rational place in a chosen uniformizer: the image of the function under completion and TauCeti.Place.completionEquivLaurentSeries.

theorem TauCeti.Place.laurentSeriesExpansion_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (z : F) : (P.laurentSeriesExpansion hP ht) z = (P.completionEquivLaurentSeries hP ht) (P.completionEmbedding z)

The Laurent expansion of a function is the Laurent expansion of its image in the completion.

noncomputable def TauCeti.Place.laurentCoeff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) : F →ₗ[k] k

The n-th Laurent coefficient of a function at the rational place, with respect to t.

@[simp]

theorem TauCeti.Place.laurentCoeff_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) (z : F) : (P.laurentCoeff hP ht n) z = ((P.laurentSeriesExpansion hP ht) z).coeff n

The Laurent coefficient is the corresponding coefficient of the Laurent expansion.

theorem TauCeti.Place.completionLaurentCoeff_completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) (z : F) : (P.completionLaurentCoeff hP ht n) (P.completionEmbedding z) = (P.laurentCoeff hP ht n) z

Completion preserves the Laurent coefficients of a function.

@[simp]

theorem TauCeti.Place.laurentSeriesExpansion_coe {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (x : ↥P.integers) : (P.laurentSeriesExpansion hP ht) ↑x = (HahnSeries.ofPowerSeries ℤ k) ((P.powerSeriesExpansion hP ht) x)

The Laurent expansion of an integral function is its power-series expansion.

theorem TauCeti.Place.laurentSeriesExpansion_zpow_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) : (P.laurentSeriesExpansion hP ht) (t ^ n) = (HahnSeries.single n) 1

Every integer power of the chosen uniformizer expands as the corresponding monomial.

@[simp]

theorem TauCeti.Place.laurentSeriesExpansion_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : (P.laurentSeriesExpansion hP ht) t = (HahnSeries.single 1) 1

The chosen uniformizer expands as the Laurent variable T.

@[simp]

theorem TauCeti.Place.valuation_laurentSeriesExpansion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (z : F) : Valued.v ((P.laurentSeriesExpansion hP ht) z) = P.valuation z

Laurent expansion carries the valuation of P to the T-adic valuation.

theorem TauCeti.Place.coeff_laurentSeriesExpansion_eq_zero_of_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {m : ℤ} {z : F} (hz : z ∈ P.filtration m) {i : ℤ} (hi : i < m) : ((P.laurentSeriesExpansion hP ht) z).coeff i = 0

A function vanishing to order at least m has no Laurent coefficients below m.

theorem TauCeti.Place.coeff_laurentSeriesExpansion_eq_of_sub_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {m : ℤ} {z w : F} (h : z - w ∈ P.filtration m) {i : ℤ} (hi : i < m) : ((P.laurentSeriesExpansion hP ht) z).coeff i = ((P.laurentSeriesExpansion hP ht) w).coeff i

The Laurent coefficients below m depend only on the function modulo the m-th order filtration.

theorem TauCeti.Place.coeff_laurentSeriesExpansion_sum {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (s : Finset ℤ) (c : ℤ → k) (i : ℤ) : ((P.laurentSeriesExpansion hP ht) (∑ j ∈ s, (algebraMap k F) (c j) * t ^ j)).coeff i = if i ∈ s then c i else 0

A finite Laurent polynomial in the uniformizer expands with its own coefficients.

theorem TauCeti.Place.coeff_laurentSeriesExpansion_eq_of_sub_sum_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {m : ℤ} {z : F} (s : Finset ℤ) (c : ℤ → k) (h : z - ∑ j ∈ s, (algebraMap k F) (c j) * t ^ j ∈ P.filtration m) {i : ℤ} (hi : i < m) : ((P.laurentSeriesExpansion hP ht) z).coeff i = if i ∈ s then c i else 0

Uniqueness of finite Laurent expansions: if a function agrees with ∑ cⱼ tʲ modulo the m-th order filtration, then its Laurent coefficients below m are the cⱼ, read as zero outside the summation range.

theorem TauCeti.Place.coeff_laurentSeriesExpansion_eq_coeff_powerSeriesExpansion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) {z : F} (hz : t ^ n * z ∈ P.integers) (i : ℕ) : ((P.laurentSeriesExpansion hP ht) z).coeff (↑i - n) = (PowerSeries.coeff i) ((P.powerSeriesExpansion hP ht) ⟨t ^ n * z, hz⟩)

Multiplying by t ^ n to make a function integral shifts its Laurent coefficients onto the coefficients of a power-series expansion.

theorem TauCeti.Place.laurentCoeff_ext_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {x y : F} : x = y ↔ ∀ (n : ℤ), (P.laurentCoeff hP ht n) x = (P.laurentCoeff hP ht n) y

Functions are equal exactly when all coefficients of their Laurent expansions at a rational place agree.

theorem TauCeti.Place.laurentCoeff_algebraMap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) (c : k) : (P.laurentCoeff hP ht n) ((algebraMap k F) c) = if n = 0 then c else 0

A constant c expands as itself: its only nonzero Laurent coefficient is c, in degree zero.

theorem TauCeti.Place.mem_filtration_iff_forall_laurentCoeff_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {m : ℤ} {z : F} : z ∈ P.filtration m ↔ ∀ n < m, (P.laurentCoeff hP ht n) z = 0

A function vanishes to order at least m at the place exactly when its Laurent coefficients below m vanish.

theorem TauCeti.Place.laurentCoeff_eq_zero_of_lt_ord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {n : ℤ} {z : F} (h : n < P.ord z) : (P.laurentCoeff hP ht n) z = 0

The Laurent coefficients of a function in degrees below its order vanish.

theorem TauCeti.Place.ord_le_of_laurentCoeff_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {n : ℤ} {z : F} (h : (P.laurentCoeff hP ht n) z ≠ 0) : P.ord z ≤ n

A nonzero Laurent coefficient bounds the order of a function from above.

theorem TauCeti.Place.laurentCoeff_ord_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {z : F} (hz : z ≠ 0) : (P.laurentCoeff hP ht (P.ord z)) z ≠ 0

The leading Laurent coefficient of a nonzero function, the one in the degree of its order, is nonzero.

theorem TauCeti.Place.sub_sum_laurentCoeff_mem_filtration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (m : ℤ) (z : F) : z - ∑ j ∈ Finset.Ico (P.ord z) m, (algebraMap k F) ((P.laurentCoeff hP ht j) z) * t ^ j ∈ P.filtration m

Truncated Laurent expansions. Removing the terms of the Laurent expansion of a function from its order up to degree m - 1 leaves a function vanishing to order at least m.

Residues

noncomputable def TauCeti.Place.residue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : F →ₗ[k] k

The residue res_{P,t} of a function at a rational place with respect to a chosen uniformizer: the coefficient of t⁻¹ in its Laurent expansion (Stichtenoth, Definition 4.2.8). It is k-linear.

theorem TauCeti.Place.residue_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (z : F) : (P.residue hP ht) z = ((P.laurentSeriesExpansion hP ht) z).coeff (-1)

The residue is the coefficient of T⁻¹ in the Laurent expansion.

theorem TauCeti.Place.completionResidue_completionEmbedding {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (z : F) : (P.completionResidue hP ht) (P.completionEmbedding z) = (P.residue hP ht) z

Completion preserves the residue of a function at the chosen uniformizer.

theorem TauCeti.Place.residue_eq_zero_of_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {z : F} (hz : z ∈ P.integers) : (P.residue hP ht) z = 0

Functions integral at the place have residue zero.

theorem TauCeti.Place.residue_eq_of_sub_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) {z w : F} (h : z - w ∈ P.integers) : (P.residue hP ht) z = (P.residue hP ht) w

The residue depends only on the function modulo integral functions.

@[simp]

theorem TauCeti.Place.residue_zpow_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℤ) : (P.residue hP ht) (t ^ n) = if n = -1 then 1 else 0

The residue of an integer power of the uniformizer.

@[simp]

theorem TauCeti.Place.residue_inv_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) : (P.residue hP ht) t⁻¹ = 1

The inverse of the uniformizer has residue one.

theorem TauCeti.Place.residue_eq_coeff_powerSeriesExpansion {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (n : ℕ) {z : F} (hz : t ^ (n + 1) * z ∈ P.integers) : (P.residue hP ht) z = (PowerSeries.coeff n) ((P.powerSeriesExpansion hP ht) ⟨t ^ (n + 1) * z, hz⟩)

If t ^ (n + 1) * z is integral, the residue of z is the degree-n coefficient of the power-series expansion of t ^ (n + 1) * z.