Power-series expansions at rational places

At a rational place with chosen uniformizer t, the compatible finite expansions define a k-algebra embedding of the valuation ring into k[[T]]. Its coefficients characterize congruence modulo every order-filtration step, so the embedding preserves orders and sends t to T. These statements do not require completeness.

References

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

noncomputable def TauCeti.Place.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) : ↥P.integers →ₐ[k] PowerSeries k

The uniformizer expansion of an integral function at a rational place, assembled from its compatible finite coefficient vectors.

Equations

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

@[simp]

theorem TauCeti.Place.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 : ℕ) (x : ↥P.integers) (i : Fin n) : (PowerSeries.coeff ↑i) ((P.powerSeriesExpansion hP ht) x) = P.truncatedExpansion hP ht n x i

Every coefficient of the infinite expansion agrees with the corresponding coefficient of any sufficiently long finite expansion.

theorem TauCeti.Place.sub_sum_coeff_powerSeriesExpansion_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) (n : ℕ) (x : ↥P.integers) : ↑x - ∑ i : Fin n, (algebraMap k F) ((PowerSeries.coeff ↑i) ((P.powerSeriesExpansion hP ht) x)) * t ^ ↑i ∈ P.filtration ↑n

Removing the first n coefficients of the power-series expansion leaves a function vanishing to order at least n.

theorem TauCeti.Place.mem_filtration_iff_coeff_powerSeriesExpansion_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) (n : ℕ) (x : ↥P.integers) : ↑x ∈ P.filtration ↑n ↔ ∀ i < n, (PowerSeries.coeff i) ((P.powerSeriesExpansion hP ht) x) = 0

Vanishing of the first n expansion coefficients is exactly membership in the n-th order filtration, including the zero function.

theorem TauCeti.Place.mem_filtration_iff_le_order_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 : ℕ) (x : ↥P.integers) : ↑x ∈ P.filtration ↑n ↔ ↑n ≤ ((P.powerSeriesExpansion hP ht) x).order

The power-series embedding identifies the local order filtration with the usual power-series order filtration.

theorem TauCeti.Place.powerSeriesExpansion_injective {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) : Function.Injective ⇑(P.powerSeriesExpansion hP ht)

Uniformizer expansion is injective even before completion: an integral function is determined by all its coefficients.

theorem TauCeti.Place.sub_mem_filtration_iff_coeff_powerSeriesExpansion_eq {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 : ℕ) (x y : ↥P.integers) : ↑x - ↑y ∈ P.filtration ↑n ↔ ∀ i < n, (PowerSeries.coeff i) ((P.powerSeriesExpansion hP ht) x) = (PowerSeries.coeff i) ((P.powerSeriesExpansion hP ht) y)

Two integral functions agree to order n precisely when their first n expansion coefficients agree.

@[simp]

theorem TauCeti.Place.powerSeriesExpansion_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.powerSeriesExpansion hP ht) ⟨t, ⋯⟩ = PowerSeries.X

The chosen uniformizer expands as the power-series variable.

theorem TauCeti.Place.order_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) (x : ↥P.integers) (hx : x ≠ 0) : ((P.powerSeriesExpansion hP ht) x).order = ↑(P.ord ↑x).toNat

The order of a nonzero integral function is the first nonzero degree of its power-series expansion.