Laurent-series expansions at rational places

The completion of a function field at a rational place is isomorphic to the Laurent-series field over the constant field. The isomorphism is the fraction-field extension of the uniformizer expansion of the completed valuation ring, so it sends a chosen uniformizer to X and restricts to the previously constructed power-series expansion on integral elements.

This supplies the local Laurent coefficients used to define residues of differentials. Keeping the construction as the canonical fraction-field extension makes its behaviour on quotients and on the valuation ring available without choosing numerator-denominator presentations.

Main results

• TauCeti.Place.completionEquivLaurentSeries: the completed local field is k((X)).
• TauCeti.Place.completionEquivLaurentSeries_apply_integer: the equivalence restricts to the power-series expansion on the completed valuation ring.
• TauCeti.Place.completionEquivLaurentSeries_uniformizer: a chosen uniformizer maps to X.
• TauCeti.Place.valuation_apply_eq_completionPlace_valuation: an isomorphism of the completion with a Laurent-series field extending a power-series expansion of the completed valuation ring preserves the valuation.
• TauCeti.Place.completionLaurentCoeff_ext_iff: Laurent coefficients determine a completed element.
• TauCeti.Place.completionResidue_completionEquivLaurentSeries_symm_derivative: completed residues kill formal derivatives.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section IV.2.

Fraction-field extensions of power-series expansions

theorem TauCeti.Place.exists_powerSeries_eq_iff_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {A : Type u_3} [Field A] {e : ↥P.completionPlace.integers ≃+* PowerSeries A} {e' : P.Completion ≃+* LaurentSeries A} (he : ∀ (x : ↥P.completionPlace.integers), e' ↑x = (HahnSeries.ofPowerSeries ℤ A) (e x)) (z : P.Completion) : (∃ (f : PowerSeries A), (HahnSeries.ofPowerSeries ℤ A) f = e' z) ↔ z ∈ P.completionPlace.integers

An isomorphism of the completion with a Laurent-series field which restricts to an isomorphism of the completed valuation ring with the power-series ring sends exactly the completed integral elements to power series.

theorem TauCeti.Place.valuation_apply_eq_completionPlace_valuation {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {A : Type u_3} [Field A] {e : ↥P.completionPlace.integers ≃+* PowerSeries A} {e' : P.Completion ≃+* LaurentSeries A} (he : ∀ (x : ↥P.completionPlace.integers), e' ↑x = (HahnSeries.ofPowerSeries ℤ A) (e x)) (x : P.Completion) : Valued.v (e' x) = P.completionPlace.valuation x

An isomorphism of the completion with a Laurent-series field over a field which restricts to an isomorphism of the completed valuation ring with the power-series ring preserves the normalized valuation.

noncomputable def TauCeti.Place.completionEquivLaurentSeries {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.Completion ≃ₐ[k] LaurentSeries k

Laurent-series expansion at a rational place. A chosen uniformizer identifies the completion of the local function field with the Laurent-series field over the constants. This is the fraction-field extension of TauCeti.Place.completionIntegersEquivPowerSeries.

@[simp]

theorem TauCeti.Place.completionEquivLaurentSeries_apply_integer {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.completionPlace.integers) : (P.completionEquivLaurentSeries hP ht) ↑x = (HahnSeries.ofPowerSeries ℤ k) ((P.completionIntegersEquivPowerSeries hP ht) x)

Laurent-series expansion restricts to power-series expansion on the completed valuation ring.

@[simp]

theorem TauCeti.Place.completionEquivLaurentSeries_symm_apply_powerSeries {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 : PowerSeries k) : (P.completionEquivLaurentSeries hP ht).symm ((HahnSeries.ofPowerSeries ℤ k) f) = ↑((P.completionIntegersEquivPowerSeries hP ht).symm f)

The inverse Laurent-series expansion restricts to the inverse power-series expansion.

@[simp]

theorem TauCeti.Place.exists_powerSeries_eq_completionEquivLaurentSeries_iff_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 : P.Completion) : (∃ (f : PowerSeries k), (HahnSeries.ofPowerSeries ℤ k) f = (P.completionEquivLaurentSeries hP ht) z) ↔ z ∈ P.completionPlace.integers

A completed function is integral exactly when its Laurent expansion comes from a power series.

@[simp]

theorem TauCeti.Place.completionEquivLaurentSeries_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.completionEquivLaurentSeries hP ht) (P.completionEmbedding t) = (HahnSeries.ofPowerSeries ℤ k) PowerSeries.X

The chosen uniformizer maps to the Laurent-series variable.

@[simp]

theorem TauCeti.Place.valuation_completionEquivLaurentSeries {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.Completion) : Valued.v ((P.completionEquivLaurentSeries hP ht) x) = P.completionPlace.valuation x

Laurent-series expansion preserves the normalized valuation. Thus the power of X at the first nonzero Laurent coefficient is the order at the original place.

@[simp]

theorem TauCeti.Place.ord_completionEquivLaurentSeries {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.Completion) : (have this := Valued.v; this).ord ((P.completionEquivLaurentSeries hP ht) x) = P.completionPlace.ord x

Laurent-series expansion preserves the additive order, including its conventional junk value 0 at the zero element.

Completed Laurent coefficients and residues

noncomputable def TauCeti.Place.completionLaurentCoeff {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.Completion →ₗ[k] k

The n-th Laurent coefficient on the completed local field, with respect to the uniformizer t.

@[simp]

theorem TauCeti.Place.completionLaurentCoeff_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 : P.Completion) : (P.completionLaurentCoeff hP ht n) z = ((P.completionEquivLaurentSeries hP ht) z).coeff n

The completed Laurent coefficient is the corresponding coefficient of the Laurent-series expansion.

theorem TauCeti.Place.completionLaurentCoeff_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 : P.Completion} : x = y ↔ ∀ (n : ℤ), (P.completionLaurentCoeff hP ht n) x = (P.completionLaurentCoeff hP ht n) y

Elements of the completed local field are equal exactly when all their Laurent coefficients are equal.

theorem TauCeti.Place.completionLaurentCoeff_completionEquivLaurentSeries_symm_single {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 n : ℤ) (c : k) : (P.completionLaurentCoeff hP ht n) ((P.completionEquivLaurentSeries hP ht).symm ((HahnSeries.single m) c)) = if n = m then c else 0

The coefficient of a Laurent monomial is zero away from its exponent.

theorem TauCeti.Place.completionLaurentCoeff_coe_integer_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) (z : ↥P.completionPlace.integers) {n : ℤ} (hn : n < 0) : (P.completionLaurentCoeff hP ht n) ↑z = 0

The negative Laurent coefficients of an integral element of the completed local field vanish.

noncomputable def TauCeti.Place.completionResidue {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.Completion →ₗ[k] k

The completed residue with respect to t, given by the coefficient of exponent -1.

@[simp]

theorem TauCeti.Place.completionResidue_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 : P.Completion) : (P.completionResidue hP ht) z = ((P.completionEquivLaurentSeries hP ht) z).coeff (-1)

The completed residue is the coefficient of exponent -1.

theorem TauCeti.Place.completionResidue_coe_integer_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) (z : ↥P.completionPlace.integers) : (P.completionResidue hP ht) ↑z = 0

The completed residue vanishes on the completed valuation ring.

theorem TauCeti.Place.completionResidue_completionEquivLaurentSeries_symm_derivative {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 : LaurentSeries k) : (P.completionResidue hP ht) ((P.completionEquivLaurentSeries hP ht).symm ((LaurentSeries.derivative k) f)) = 0

The coefficient of X⁻¹ in the formal derivative of a Laurent series is zero. Equivalently, the local residue kills formal derivatives.