Laurent expansions over the residue field, and residues at places with separable residue field

Let P be a place of F / k and let t be a uniformizer of the completion F̂_P. Through any coefficient field s of the completed valuation ring, the identification of 𝒪̂_P with F_P[[T]] (TauCeti.Place.completionIntegersEquivPowerSeriesOfSection) extends to fraction fields: F̂_P is the Laurent-series field F_P((T)), with t sent to T and the valuation of P sent to the T-adic valuation. This holds at every place, but when F_P is inseparable over k there may be no k-linear coefficient field, and then no k-linear expansion.

Now let F_P be separable over k, and let t ∈ F have order one at P. The coefficient field over k gives the k-linear identification (TauCeti.Place.completionIntegersEquivPowerSeriesResidueField), and its extension to fraction fields identifies the completion of F at P with F_P((T)) over k. Every function z ∈ F therefore has a Laurent expansion ∑ aᵢ tⁱ with coefficients aᵢ ∈ F_P, and its coefficient of t⁻¹ is the residue res_{P,t}(z) ∈ F_P. Composing with the trace of F_P / k gives a k-valued residue, the form in which residues at places of arbitrary degree enter the residue theorem and the comparison of Weil differentials with differentials.

At a rational place the coefficient field is k itself, and these expansions and residues are the ones of TauCeti.Place.laurentSeriesExpansion and TauCeti.Place.residue, read in F_P (TauCeti.Place.residueResidueField_eq_algebraMap_residue); the trace of the residue is then the residue (TauCeti.Place.traceResidue_eq_residue).

Main definitions

• TauCeti.Place.completionEquivLaurentSeriesOfSection: through a coefficient field, the completion at any place is F_P((T)).
• TauCeti.Place.completionEquivLaurentSeriesResidueField: the completion at P is F_P((T)).
• TauCeti.Place.laurentSeriesExpansionResidueField: the Laurent expansion of functions at P in t, with coefficients in F_P.
• TauCeti.Place.residueResidueField: the residue res_{P,t} : F → F_P, the coefficient of t⁻¹.
• TauCeti.Place.traceResidue: the k-valued residue Tr_{F_P/k} ∘ res_{P,t}.
• TauCeti.Place.traceResidue_mul_inv_uniformizer: for an integral numerator u, the k-valued residue of u / t is the trace of its value at P.

Main results

• TauCeti.Place.exists_completion_ringEquiv_laurentSeries: at every place, separable residue field or not, F̂_P is isomorphic to F_P((T)) by a valuation-preserving ring isomorphism.
• TauCeti.Place.mem_filtration_iff_le_order_powerSeriesExpansionResidueField: a regular function vanishes to order n exactly when its expansion has order at least n.
• TauCeti.Place.exists_trunc_powerSeriesExpansionResidueField_eq: every power series over F_P is the expansion of a regular function up to any prescribed order.
• TauCeti.Place.valuation_laurentSeriesExpansionResidueField: Laurent expansion carries the valuation of P to the T-adic valuation.
• TauCeti.Place.coeff_zero_laurentSeriesExpansionResidueField: the constant coefficient of a function regular at P is its value at P.
• TauCeti.Place.residueResidueField_mul_inv_uniformizer: res_{P,t}(u / t) = u(P) for u regular at P.
• TauCeti.Place.residueResidueField_eq_algebraMap_residue and TauCeti.Place.traceResidue_eq_residue: at a rational place these residues are the residue TauCeti.Place.residue with coefficients in k.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2, Definition 4.2.8, and Remark 4.3.7.
• J.-P. Serre, Local Fields, GTM 67, Springer, 1979, Chapter II, §4.

Laurent expansions over a coefficient field

noncomputable def TauCeti.Place.completionEquivLaurentSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) : P.Completion ≃+* LaurentSeries P.ResidueField

The completion at a place is F_P((T)). Given a coefficient field s of the completed valuation ring, a ring embedding of the residue field F_P lifting it, a uniformizer t of the completion identifies it with the Laurent-series field over the residue field, sending t to T; this is the fraction-field extension of TauCeti.Place.completionIntegersEquivPowerSeriesOfSection.

@[simp]

theorem TauCeti.Place.completionEquivLaurentSeriesOfSection_apply_integer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) : (P.completionEquivLaurentSeriesOfSection s hs ht) ↑x = (HahnSeries.ofPowerSeries ℤ P.ResidueField) ((P.completionIntegersEquivPowerSeriesOfSection s hs ht) x)

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

theorem TauCeti.Place.exists_powerSeries_eq_completionEquivLaurentSeriesOfSection_iff_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (z : P.Completion) : (∃ (f : PowerSeries P.ResidueField), (HahnSeries.ofPowerSeries ℤ P.ResidueField) f = (P.completionEquivLaurentSeriesOfSection s hs 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.completionEquivLaurentSeriesOfSection_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) : (P.completionEquivLaurentSeriesOfSection s hs ht) t = (HahnSeries.single 1) 1

The uniformizer expands as the Laurent variable T.

theorem TauCeti.Place.completionEquivLaurentSeriesOfSection_section {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (a : P.ResidueField) : (P.completionEquivLaurentSeriesOfSection s hs ht) ↑(s a) = HahnSeries.C a

The coefficient field expands to the constant Laurent series.

@[simp]

theorem TauCeti.Place.valuation_completionEquivLaurentSeriesOfSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (s : P.ResidueField →+* ↥P.completionPlace.integers) (hs : ∀ (a : P.ResidueField), (IsLocalRing.residue ↥P.completionPlace.integers) (s a) = P.residueFieldEquivCompletion a) {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : P.Completion) : Valued.v ((P.completionEquivLaurentSeriesOfSection s hs ht) x) = P.completionPlace.valuation x

Laurent-series expansion preserves the normalized valuation.

theorem TauCeti.Place.exists_completion_ringEquiv_laurentSeries {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : ∃ (e : P.Completion ≃+* LaurentSeries P.ResidueField), ∀ (x : P.Completion), Valued.v (e x) = P.completionPlace.valuation x

At every place the completion is F_P((T)), separable residue field or not: some isomorphism of the completion with the Laurent-series field over the residue field carries the valuation of P to the T-adic valuation. When F_P is inseparable over k there may be no k-linear such isomorphism (TauCeti.Place.isEmpty_completion_algEquiv_laurentSeries).

Laurent expansions in the completion

noncomputable def TauCeti.Place.completionEquivLaurentSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) : P.Completion ≃ₐ[k] LaurentSeries P.ResidueField

The completion at a place with separable residue field is F_P((T)). A uniformizer t of the completion identifies it with the Laurent-series field over the residue field, sending t to T; this is the fraction-field extension of TauCeti.Place.completionIntegersEquivPowerSeriesResidueField.

@[simp]

theorem TauCeti.Place.completionEquivLaurentSeriesResidueField_apply_integer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : ↥P.completionPlace.integers) : (P.completionEquivLaurentSeriesResidueField ht) ↑x = (HahnSeries.ofPowerSeries ℤ P.ResidueField) ((P.completionIntegersEquivPowerSeriesResidueField ht) x)

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

theorem TauCeti.Place.exists_powerSeries_eq_completionEquivLaurentSeriesResidueField_iff_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (z : P.Completion) : (∃ (f : PowerSeries P.ResidueField), (HahnSeries.ofPowerSeries ℤ P.ResidueField) f = (P.completionEquivLaurentSeriesResidueField 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.completionEquivLaurentSeriesResidueField_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) : (P.completionEquivLaurentSeriesResidueField ht) t = (HahnSeries.single 1) 1

The uniformizer expands as the Laurent variable T.

theorem TauCeti.Place.completionEquivLaurentSeriesResidueField_completionResidueFieldSection {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (a : P.ResidueField) : (P.completionEquivLaurentSeriesResidueField ht) ↑(P.completionResidueFieldSection a) = HahnSeries.C a

The coefficient field expands to the constant Laurent series.

@[simp]

theorem TauCeti.Place.valuation_completionEquivLaurentSeriesResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : P.Completion} (ht : P.completionPlace.ord t = 1) (x : P.Completion) : Valued.v ((P.completionEquivLaurentSeriesResidueField ht) x) = P.completionPlace.valuation x

Laurent-series expansion preserves the normalized valuation.

Expansions of functions

noncomputable def TauCeti.Place.powerSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) : ↥P.integers →ₐ[k] PowerSeries P.ResidueField

The power-series expansion of a function regular at a place with separable residue field in a chosen uniformizer t, with coefficients in the residue field: the image of the function under completion and TauCeti.Place.completionIntegersEquivPowerSeriesResidueField.

theorem TauCeti.Place.powerSeriesExpansionResidueField_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (x : ↥P.integers) : (P.powerSeriesExpansionResidueField ht) x = (P.completionIntegersEquivPowerSeriesResidueField ⋯) (P.completionIntegersEmbedding x)

The power-series expansion of a function is the expansion of its image in the completed valuation ring.

@[simp]

theorem TauCeti.Place.constantCoeff_powerSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (x : ↥P.integers) : PowerSeries.constantCoeff ((P.powerSeriesExpansionResidueField ht) x) = (IsLocalRing.residue ↥P.integers) x

The constant coefficient of the power-series expansion of a function regular at P is its value at P.

theorem TauCeti.Place.mem_filtration_iff_le_order_powerSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (n : ℕ) (x : ↥P.integers) : ↑x ∈ P.filtration ↑n ↔ ↑n ≤ ((P.powerSeriesExpansionResidueField ht) x).order

A function regular at P vanishes to order at least n exactly when its power-series expansion has order at least n.

@[simp]

theorem TauCeti.Place.powerSeriesExpansionResidueField_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) : (P.powerSeriesExpansionResidueField ht) ⟨t, ⋯⟩ = PowerSeries.X

The chosen uniformizer expands as the power-series variable.

theorem TauCeti.Place.exists_trunc_powerSeriesExpansionResidueField_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (g : PowerSeries P.ResidueField) (n : ℕ) : ∃ (x : ↥P.integers), (PowerSeries.trunc n) ((P.powerSeriesExpansionResidueField ht) x) = (PowerSeries.trunc n) g

Expansions are onto modulo Tⁿ: every power series over the residue field agrees with the expansion of some function regular at P up to order n.

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

The Laurent expansion of a function at a place with separable residue field in a chosen uniformizer t, with coefficients in the residue field: the image of the function under completion and TauCeti.Place.completionEquivLaurentSeriesResidueField.

theorem TauCeti.Place.laurentSeriesExpansionResidueField_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (z : F) : (P.laurentSeriesExpansionResidueField ht) z = (P.completionEquivLaurentSeriesResidueField ⋯) (P.completionEmbedding z)

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

@[simp]

theorem TauCeti.Place.laurentSeriesExpansionResidueField_coe {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (x : ↥P.integers) : (P.laurentSeriesExpansionResidueField ht) ↑x = (HahnSeries.ofPowerSeries ℤ P.ResidueField) ((P.powerSeriesExpansionResidueField ht) x)

The Laurent expansion of a function regular at P is its power-series expansion.

theorem TauCeti.Place.laurentSeriesExpansionResidueField_zpow_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (n : ℤ) : (P.laurentSeriesExpansionResidueField ht) (t ^ n) = (HahnSeries.single n) 1

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

@[simp]

theorem TauCeti.Place.laurentSeriesExpansionResidueField_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) : (P.laurentSeriesExpansionResidueField ht) t = (HahnSeries.single 1) 1

The chosen uniformizer expands as the Laurent variable T.

@[simp]

theorem TauCeti.Place.valuation_laurentSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (z : F) : Valued.v ((P.laurentSeriesExpansionResidueField ht) z) = P.valuation z

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

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

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

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

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

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

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

theorem TauCeti.Place.coeff_zero_laurentSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (x : ↥P.integers) : ((P.laurentSeriesExpansionResidueField ht) ↑x).coeff 0 = (IsLocalRing.residue ↥P.integers) x

The constant coefficient of the Laurent expansion of a function regular at P is its value at P.

Residues

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

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

theorem TauCeti.Place.residueResidueField_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (z : F) : (P.residueResidueField ht) z = ((P.laurentSeriesExpansionResidueField ht) z).coeff (-1)

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

theorem TauCeti.Place.residueResidueField_eq_zero_of_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) {z : F} (hz : z ∈ P.integers) : (P.residueResidueField ht) z = 0

Functions integral at the place have residue zero.

theorem TauCeti.Place.residueResidueField_eq_of_sub_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) {z w : F} (h : z - w ∈ P.integers) : (P.residueResidueField ht) z = (P.residueResidueField ht) w

The residue depends only on the function modulo integral functions.

@[simp]

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

The residue of an integer power of the uniformizer.

@[simp]

theorem TauCeti.Place.residueResidueField_inv_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) : (P.residueResidueField ht) t⁻¹ = 1

The inverse of the uniformizer has residue one.

theorem TauCeti.Place.residueResidueField_eq_coeff_powerSeriesExpansionResidueField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (n : ℕ) {z : F} (hz : t ^ (n + 1) * z ∈ P.integers) : (P.residueResidueField ht) z = (PowerSeries.coeff n) ((P.powerSeriesExpansionResidueField 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.

@[simp]

theorem TauCeti.Place.residueResidueField_mul_inv_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (u : ↥P.integers) : (P.residueResidueField ht) (↑u * t⁻¹) = (IsLocalRing.residue ↥P.integers) u

The residue of u / t is the value of u at P for a function u regular at P.

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

The k-valued residue at a place with separable residue field: the trace from F_P to k of the residue res_{P,t} (Stichtenoth, Remark 4.3.7).

This is the classical residue-field trace precisely when Module.Finite k P.ResidueField, which TauCeti.Place.finiteDimensional_residueField supplies for every place of a function field. Absent that, Algebra.trace is the junk value 0 (Algebra.trace_eq_zero_of_not_exists_basis), the convention TauCeti.Place.normResidue and TauCeti.Place.degree follow as well.

theorem TauCeti.Place.traceResidue_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (z : F) : (P.traceResidue ht) z = (Algebra.trace k P.ResidueField) ((P.residueResidueField ht) z)

The k-valued residue is the trace of the residue.

theorem TauCeti.Place.traceResidue_mul_inv_uniformizer {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (u : ↥P.integers) : (P.traceResidue ht) (↑u * t⁻¹) = (Algebra.trace k P.ResidueField) ((IsLocalRing.residue ↥P.integers) u)

The trace residue of u / t is the trace of the value of u at P, for a function u regular at P. This is the k-valued form of TauCeti.Place.residueResidueField_mul_inv_uniformizer, used when local components are expressed as trace residues at places with nontrivial residue field.

Comparison with residues at rational places

theorem TauCeti.Place.powerSeriesExpansionResidueField_eq_map {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (hP : P.degree = 1) (x : ↥P.integers) : (P.powerSeriesExpansionResidueField ht) x = (PowerSeries.map (algebraMap k P.ResidueField)) ((P.powerSeriesExpansion hP ht) x)

At a rational place, the power-series expansion in the residue field is the power-series expansion over k, read in F_P.

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

At a rational place, Laurent coefficients in the residue field are the Laurent coefficients over k, read in F_P.

theorem TauCeti.Place.residueResidueField_eq_algebraMap_residue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) (hP : P.degree = 1) (z : F) : (P.residueResidueField ht) z = (algebraMap k P.ResidueField) ((P.residue hP ht) z)

At a rational place the residue in the residue field is the residue over k, read in F_P.

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

At a rational place the k-valued residue is the residue over k.