Residues under a change of uniformizer

Let P be a rational place of F / k and let s and t both have order one at P. The residue of a function z with respect to s can be computed from Laurent expansions in t:

res_{P,s}(z) = coeff_{-1} (z(T) * s'(T)),

where z(T) and s(T) are the Laurent expansions of z and s in t and s'(T) is the formal derivative. This is the expansion-level form of Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt) (Proposition 4.2.9). As a corollary, whenever a function w has expansion s'(T) in t, res_{P,s}(z) = res_{P,t}(z * w). The function-field derivative ds/dt is such a w when t is separating (TauCeti.Place.laurentSeriesExpansion_derivativeOfSeparating), which gives the formula in Stichtenoth's form (TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating).

The formula holds in every characteristic. Both sides are k-linear in z and vanish on functions integral at P, so it suffices to compare them on the negative powers s ^ j. There it is the formal identity PowerSeries.coeff_neg_one_coe_zpow_mul_derivative for the expansion of s, a power series of order one.

The same formula holds at every place P whose residue field F_P is separable over k, for the F_P-valued residues res_{P,s} and res_{P,t} (TauCeti.Place.residueResidueField) and the Laurent expansions with coefficients in F_P, hence also for the k-valued residues Tr_{F_P/k} ∘ res_{P,t} (TauCeti.Place.traceResidue). Here the expansions in s and in t are two identifications of the completion at P with F_P((T)). Both send the coefficient field of the completion to the constants, so the expansion in t of a function, read as a series in its expansion in s, is a substitution T ↦ s(T) fixing F_P. Such a substitution preserves residues (LaurentSeries.coeff_neg_one_map_mul_derivative).

Main results

• TauCeti.Place.residue_eq_coeff_laurentSeriesExpansion_mul_derivative: the residue with respect to s, computed from Laurent expansions in t.
• TauCeti.Place.residue_eq_residue_mul: res_{P,s}(z) = res_{P,t}(z * w) for a function w whose expansion in t is the derivative of that of s.
• TauCeti.Place.residueResidueField_eq_coeff_laurentSeriesExpansionResidueField_mul_derivative and TauCeti.Place.residueResidueField_eq_residueResidueField_mul: the same at a place with separable residue field, with residues and coefficients in F_P.
• TauCeti.Place.traceResidue_eq_traceResidue_mul: the same for the k-valued residues.

References

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

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

Change of uniformizer for residues. At a rational place, the residue with respect to a uniformizer s is the coefficient of T⁻¹ in z(T) * s'(T), where z(T) and s(T) are the Laurent expansions of z and s in another uniformizer t (Stichtenoth, Proposition 4.2.9).

theorem TauCeti.Place.residue_eq_residue_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {s t : F} (hP : P.degree = 1) (ht : P.ord t = 1) (hs : P.ord s = 1) {w : F} (hw : (P.laurentSeriesExpansion hP ht) w = (LaurentSeries.derivative k) ((P.laurentSeriesExpansion hP ht) s)) (z : F) : (P.residue hP hs) z = (P.residue hP ht) (z * w)

Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt): if the Laurent expansion of w in t is the derivative of that of s, then the residue of z with respect to s is the residue of z * w with respect to t.

Places with separable residue field

theorem TauCeti.Place.coeff_neg_one_completionEquivLaurentSeriesResidueField_mul_derivative {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) [Algebra.IsSeparable k P.ResidueField] {s t : P.Completion} (hs : P.completionPlace.ord s = 1) (ht : P.completionPlace.ord t = 1) (z : P.Completion) : ((P.completionEquivLaurentSeriesResidueField ht) z * (LaurentSeries.derivative P.ResidueField) ((P.completionEquivLaurentSeriesResidueField ht) s)).coeff (-1) = ((P.completionEquivLaurentSeriesResidueField hs) z).coeff (-1)

Change of uniformizer in the completion. At a place with separable residue field, the coefficient of T⁻¹ in the expansion of a completed function z in a uniformizer s is the coefficient of T⁻¹ in z(T) * s'(T), where z(T) and s(T) are the expansions in another uniformizer t, all with coefficients in F_P.

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

Change of uniformizer for residues at a place with separable residue field. The residue res_{P,s}(z) ∈ F_P is the coefficient of T⁻¹ in z(T) * s'(T), where z(T) and s(T) are the Laurent expansions of z and s in another uniformizer t, with coefficients in F_P (Stichtenoth, Proposition 4.2.9).

theorem TauCeti.Place.residueResidueField_eq_residueResidueField_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {s t : F} (ht : P.ord t = 1) [Algebra.IsSeparable k P.ResidueField] (hs : P.ord s = 1) {w : F} (hw : (P.laurentSeriesExpansionResidueField ht) w = (LaurentSeries.derivative P.ResidueField) ((P.laurentSeriesExpansionResidueField ht) s)) (z : F) : (P.residueResidueField hs) z = (P.residueResidueField ht) (z * w)

The transformation formula res_{P,s}(z) = res_{P,t}(z · w) at a place with separable residue field, for a function w whose Laurent expansion in t is the derivative of that of s.

theorem TauCeti.Place.traceResidue_eq_traceResidue_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) {s t : F} (ht : P.ord t = 1) [Algebra.IsSeparable k P.ResidueField] (hs : P.ord s = 1) {w : F} (hw : (P.laurentSeriesExpansionResidueField ht) w = (LaurentSeries.derivative P.ResidueField) ((P.laurentSeriesExpansionResidueField ht) s)) (z : F) : (P.traceResidue hs) z = (P.traceResidue ht) (z * w)

The transformation formula for k-valued residues Tr_{F_P/k} res_{P,s}(z) = Tr_{F_P/k} res_{P,t}(z · w), for a function w whose Laurent expansion in t is the derivative of that of s.