Truncated uniformizer expansions at rational places

Let P be a rational place of F / k and let t have order one at P. Every function integral at P has a unique expansion modulo the n-th order filtration as a polynomial in t with n coefficients in k. This file constructs these finite coefficient vectors and characterizes them by the order of the remainder. The coefficients depend only on the function modulo the same filtration, and successive truncations agree. Constants have only a constant coefficient, the chosen uniformizer has only a degree-one coefficient, and multiplication of integral functions gives coefficient convolution.

These are finite truncations: no completeness assumption or infinite series is used. They provide the finite approximation and uniqueness statements for the power-series construction in a completed valuation ring. In particular, the statements also apply to the place on a completion once that place and its constant-field algebra have been supplied.

References

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

theorem TauCeti.Place.existsUnique_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) (n : ℕ) (x : F) (hx : x ∈ P.integers) : ∃! c : Fin n → k, x - ∑ i : Fin n, (algebraMap k F) (c i) * t ^ ↑i ∈ P.filtration ↑n

At a rational place, an integral function has a unique polynomial expansion of length n in a chosen uniformizer, with remainder vanishing to order at least n. The filtration condition includes the zero remainder, unlike an unguarded inequality for ord.

Canonical finite coefficient vectors

noncomputable def TauCeti.Place.truncatedExpansion {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) : Fin n → k

The coefficients of the unique length-n uniformizer expansion of an integral function at a rational place. Its remainder is characterized by TauCeti.Place.truncatedExpansion_eq_iff; successive lengths agree on their common indices.

Equations

• P.truncatedExpansion hP ht n x = ⋯.choose

theorem TauCeti.Place.sub_sum_truncatedExpansion_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) (P.truncatedExpansion hP ht n x i) * t ^ ↑i ∈ P.filtration ↑n

Subtracting the truncated expansion leaves a function vanishing to the stated order.

theorem TauCeti.Place.truncatedExpansion_eq_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) (n : ℕ) (x : ↥P.integers) (c : Fin n → k) : P.truncatedExpansion hP ht n x = c ↔ ↑x - ∑ i : Fin n, (algebraMap k F) (c i) * t ^ ↑i ∈ P.filtration ↑n

A coefficient vector is the truncated expansion precisely when its remainder vanishes to order at least the length of the vector. This characterizes the coefficients without unfolding their construction.

@[simp]

theorem TauCeti.Place.truncatedExpansion_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 : ℕ) : P.truncatedExpansion hP ht n 0 = 0

The zero function has zero coefficients at every truncation length.

@[simp]

theorem TauCeti.Place.truncatedExpansion_add {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) : P.truncatedExpansion hP ht n (x + y) = P.truncatedExpansion hP ht n x + P.truncatedExpansion hP ht n y

Uniformizer coefficients respect addition of integral functions.

@[simp]

theorem TauCeti.Place.truncatedExpansion_smul {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) (x : ↥P.integers) : P.truncatedExpansion hP ht n (c • x) = c • P.truncatedExpansion hP ht n x

Uniformizer coefficients respect multiplication by constants.

@[simp]

theorem TauCeti.Place.truncatedExpansion_neg {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) : P.truncatedExpansion hP ht n (-x) = -P.truncatedExpansion hP ht n x

Uniformizer coefficients respect negation of integral functions.

@[simp]

theorem TauCeti.Place.truncatedExpansion_sub {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) : P.truncatedExpansion hP ht n (x - y) = P.truncatedExpansion hP ht n x - P.truncatedExpansion hP ht n y

Uniformizer coefficients respect subtraction of integral functions.

@[simp]

theorem TauCeti.Place.truncatedExpansion_one {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.truncatedExpansion hP ht n 1 = fun (i : Fin n) => if ↑i = 0 then 1 else 0

The unit has constant coefficient one and all positive-degree coefficients zero.

@[simp]

theorem TauCeti.Place.truncatedExpansion_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.truncatedExpansion hP ht n ((algebraMap k ↥P.integers) c) = fun (i : Fin n) => if ↑i = 0 then c else 0

Constants have their given constant coefficient and zero positive-degree coefficients.

@[simp]

theorem TauCeti.Place.truncatedExpansion_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.truncatedExpansion hP ht n ⟨t, ⋯⟩ = fun (i : Fin n) => if ↑i = 1 then 1 else 0

The chosen uniformizer has coefficient one in degree one and zero in every other degree, including at truncation lengths zero and one.

@[simp]

theorem TauCeti.Place.truncatedExpansion_mul {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) (i : Fin n) : P.truncatedExpansion hP ht n (x * y) i = ∑ j : Fin n × Fin n with ↑j.1 + ↑j.2 = ↑i, P.truncatedExpansion hP ht n x j.1 * P.truncatedExpansion hP ht n y j.2

The coefficient of a product is the convolution of the coefficients of its factors. The sum ranges over bounded pairs of indices whose degrees add to the requested degree; terms of degree at least n vanish modulo the n-th order filtration.

@[simp]

theorem TauCeti.Place.truncatedExpansion_castSucc {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) : P.truncatedExpansion hP ht (n + 1) x i.castSucc = P.truncatedExpansion hP ht n x i

Increasing the truncation length preserves every coefficient already extracted. This compatibility allows the finite vectors to determine a single power-series coefficient sequence.

@[simp]

theorem TauCeti.Place.truncatedExpansion_castLE {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 m : ℕ} (hnm : n ≤ m) (x : ↥P.integers) (i : Fin n) : P.truncatedExpansion hP ht m x (Fin.castLE hnm i) = P.truncatedExpansion hP ht n x i

Increasing the truncation length preserves the coefficients at all indices of the shorter expansion.

theorem TauCeti.Place.truncatedExpansion_eq_iff_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) (n : ℕ) (x y : ↥P.integers) : P.truncatedExpansion hP ht n x = P.truncatedExpansion hP ht n y ↔ ↑x - ↑y ∈ P.filtration ↑n

Two integral functions have the same length-n coefficient vector exactly when they agree modulo the n-th order filtration. Thus coefficient extraction descends to finite jets, with no choices of representatives visible in the coefficients.