Laurent expansions of derivatives, and residues of differentials #
Let P be a rational place of F / k and let t have order one at P, with F separable over
k(t). Differentiation with respect to t (TauCeti.derivativeOfSeparating) is then compatible
with Laurent expansion in t: the expansion of dz/dt is the formal derivative of the expansion
of z. Both sides are k-derivations of F into k((T)) taking t to 1, and a derivation of
F is determined by its value at a separating element
(Derivation.apply_eq_derivativeOfSeparating_smul).
This identifies the function-field derivative ds/dt with the series s'(T) used in the
change-of-uniformizer formula (TauCeti.Place.residue_eq_residue_mul), giving Stichtenoth's
transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt) for two uniformizers s and t
(Proposition 4.2.9). It holds in every characteristic.
The formula makes the residue of a Kähler differential well defined (Definition 4.2.10). Writing
ω = z dt, the residue res_P(ω) := res_{P,t}(z) does not depend on the separating uniformizer
t, since z dt = (z · dt/ds) ds. An exact differential dy has residue zero, because the formal
derivative of a Laurent series has no T⁻¹ term.
Over a perfect field every prime element of a place is separating
(TauCeti.Place.transcendental_and_isSeparable_adjoin_of_ord_eq_one), so the residue of a
differential at a rational place needs no choice of uniformizer at all:
TauCeti.Place.kaehlerResidueOfPerfectField computes it with any prime element.
The compatibility of expansions with derivatives holds for every k-algebra map F → A((X))
sending t to X (TauCeti.algHom_derivativeOfSeparating), so it also holds at a place of any
degree whose residue field F_P is separable over k, for the expansion with coefficients in
F_P (TauCeti.Place.laurentSeriesExpansionResidueField).
The derivation z ↦ (e z)' of such an expansion e sends t to 1, so dt ≠ 0 in Ω[F⁄k]
(TauCeti.D_ne_zero_of_algHom_laurentSeries). Hence at a place whose residue field is separable
over k every uniformizer has a nonzero differential, over any constant field
(TauCeti.Place.D_ne_zero_of_ord_eq_one). When F / k has a separating element, the Kähler
differentials form a line, and so every uniformizer at such a place is separating
(TauCeti.Place.isSeparable_adjoin_of_ord_eq_one). This needs no perfect constant field: over an
imperfect field it supplies separating uniformizers wherever the residue field is separable.
The compatibility of expansions with derivatives gives the order of a derivative at such a place:
if z vanishes to order at least m at P, then dz/dt ≡ m z / t modulo functions
vanishing to order at least m, and iterating, dⁱz/dtⁱ is congruent to
m (m - 1) ⋯ (m - i + 1) z / tⁱ. In particular, for a separating uniformizer t at such a
place P, dz/dt is integral at P whenever z is. This is the local input for computing
orders of Wronskians, and for comparing regular Kähler differentials with regular Weil
differentials.
The transformation formula and the residue of a differential also carry over to a place P of
arbitrary degree whose residue field F_P is separable over k, with Laurent expansions and
residues taking values in F_P
(TauCeti.Place.laurentSeriesExpansionResidueField, TauCeti.Place.residueResidueField).
The residue res_P(ω) ∈ F_P of a Kähler differential is again well defined, and so is its trace
Tr_{F_P/k} res_P(ω) ∈ k, the k-valued residue at a place of higher degree (Stichtenoth,
Remark 4.3.7). At a rational place the latter is the residue TauCeti.Place.kaehlerResidue.
Main definitions #
TauCeti.Place.kaehlerResidue: the residueres_P(ω)of a Kähler differentialωat a rational place, computed with a separating uniformizer.TauCeti.Place.kaehlerResidueOfPerfectField: the residueres_P(ω)at a rational place of a function field over a perfect field, with no uniformizer in its signature.TauCeti.Place.kaehlerResidueResidueField: the residueres_P(ω) ∈ F_Pat a place with separable residue field, computed with a separating uniformizer.TauCeti.Place.kaehlerTraceResidue: its traceTr_{F_P/k} res_P(ω) ∈ k.
Main results #
TauCeti.algHom_derivativeOfSeparating: ak-algebra mapF → A((X))sendingttoXcarriesdz/dtto the formal derivative.TauCeti.Place.D_ne_zero_of_ord_eq_one: a uniformizer at a place with separable residue field has a nonzero differential.TauCeti.Place.isSeparable_adjoin_of_ord_eq_one: every uniformizer at a place with separable residue field is separating, whenF / khas a separating element.TauCeti.Place.laurentSeriesExpansion_derivativeOfSeparating: the Laurent expansion ofdz/dtintis the derivative of the Laurent expansion ofz.TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating: the transformation formulares_{P,s}(z) = res_{P,t}(z · ds/dt).TauCeti.Place.residue_derivativeOfSeparating:res_{P,t}(dy/dt) = 0.TauCeti.Place.laurentSeriesExpansionResidueField_derivativeOfSeparating: at a place with separable residue field, the Laurent expansion ofdz/dtwith coefficients inF_Pis the derivative of the Laurent expansion ofz.TauCeti.Place.derivativeOfSeparating_mem_integers: for a separating uniformizertat a placePwith separable residue field,dz/dtis integral atPwheneverzis.TauCeti.Place.iterate_derivativeOfSeparating_sub_zsmul_mem_filtration: ifzvanishes to order at leastm, thendⁱz/dtⁱ ≡ m (m - 1) ⋯ (m - i + 1) z / tⁱmodulo orderm - i + 1.TauCeti.Place.normalized_entry_sub_mem_filtration_one: normalizing thei-th iterated derivative of a nonzerofbytⁱ / fgives(descPochhammer ℤ i).eval (ord f)modulo the maximal ideal.TauCeti.Place.kaehlerResidue_eq_kaehlerResidue: the residue of a differential is independent of the uniformizer used to compute it.TauCeti.Place.kaehlerResidue_D: exact differentials have residue zero.TauCeti.Place.kaehlerResidueOfPerfectField_smul_D: over a perfect field,res_P(z dt)isres_{P,t}(z)for every prime elementt.TauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating: the transformation formula at a place with separable residue field.TauCeti.Place.kaehlerResidueResidueField_eq_kaehlerResidueResidueFieldandTauCeti.Place.kaehlerTraceResidue_eq_kaehlerTraceResidue: there too, the residue of a differential is independent of the uniformizer used to compute it.TauCeti.Place.kaehlerTraceResidue_eq_kaehlerResidue: at a rational place thek-valued residue isTauCeti.Place.kaehlerResidue.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2, Proposition 4.2.9 and Definition 4.2.10, and Remark 4.3.7.
Laurent expansions of derivatives. Let t be a separating element of F / k and let
e : F → A((X)) be a k-algebra map into Laurent series over a k-algebra A with e t = X.
Then e carries dz/dt to the formal derivative of e z.
The Laurent expansion of a derivative. At a rational place P at which the separating
element t has order one, the Laurent expansion in t of dz/dt is the formal derivative of the
Laurent expansion of z.
Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt) for two
uniformizers s and t at a rational place, with t separating (Proposition 4.2.9).
The derivative dy/dt has residue zero with respect to t: the formal derivative of a
Laurent series has no T⁻¹ term.
Expansions with coefficients in the residue field #
The Laurent expansion of a derivative, at a place of any degree. At a place P whose
residue field is separable over k, with t separating and of order one at P, the Laurent
expansion in t of dz/dt, with coefficients in the residue field, is the formal derivative of
the Laurent expansion of z.
Orders of derivatives #
The leading term of a derivative. If z vanishes to order at least m at P, then
dz/dt ≡ m z / t modulo functions vanishing to order at least m. This holds in every
characteristic.
Differentiation with respect to a separating uniformizer preserves the valuation ring at a place with separable residue field, in every characteristic.
Differentiation with respect to a prime element lowers the order at P by at most one.
The i-th derivative with respect to a prime element lowers the order at P by at most
i.
The leading term of an iterated derivative. If z vanishes to order at least m at P,
then dⁱz/dtⁱ ≡ m (m - 1) ⋯ (m - i + 1) z / tⁱ modulo functions vanishing to order at least
m - i + 1. The coefficient is the descending Pochhammer symbol evaluated at m.
Normalizing the entry of the Wronskian matrix of a nonzero function f by t ^ i / f gives
the integer (descPochhammer ℤ i).eval (ord f), up to the maximal ideal of P.
Separating uniformizers #
A uniformizer has a nonzero differential. At a place P whose residue field is separable
over k, an element t of order one at P has dt ≠ 0 in Ω[F⁄k]. Neither a perfect constant
field nor a separating element is needed.
Every uniformizer is separating at a place P whose residue field is separable over k,
provided F / k has some separating element x: an element t of order one at P makes F
separable over k(t). The element t is transcendental over k by
TauCeti.Place.transcendental_of_ord_ne_zero.
Over a perfect constant field both hypotheses hold automatically; there
TauCeti.Place.transcendental_and_isSeparable_adjoin_of_ord_eq_one gives the same conclusion.
Residues of Kähler differentials #
The residue res_P(ω) of a Kähler differential ω at a rational place P
(Stichtenoth, Definition 4.2.10): writing ω = z dt for a separating uniformizer t at P, it
is the residue res_{P,t}(z). It does not depend on t
(TauCeti.Place.kaehlerResidue_eq_kaehlerResidue).
Instances For
The residue of ω is the residue of its coordinate ω / dt in the basis dt.
The residue of z dt is res_{P,t}(z).
Exact differentials have residue zero: res_P(dy) = 0.
The residue of a differential is well defined (Stichtenoth, Definition 4.2.10): it does not depend on the separating uniformizer used to compute it.
Residues of Kähler differentials over a perfect field #
The residue res_P(ω) of a Kähler differential ω at a rational place P of a function
field over a perfect field (Stichtenoth, Definition 4.2.10). Over a perfect field every prime
element of P is separating
(TauCeti.Place.transcendental_and_isSeparable_adjoin_of_ord_eq_one), so this is
TauCeti.Place.kaehlerResidue computed with some prime element; it does not depend on the choice
(TauCeti.Place.kaehlerResidueOfPerfectField_eq_kaehlerResidue).
Instances For
Over a perfect field, the residue of a differential is TauCeti.Place.kaehlerResidue computed
with any separating uniformizer.
Over a perfect field, the residue of z dt is res_{P,t}(z) for every prime element t
of P.
Exact differentials have residue zero: res_P(dy) = 0.
Places with separable residue field #
Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt) at a place
with separable residue field, for two uniformizers s and t with t separating, the residues
taking values in F_P (Proposition 4.2.9).
The transformation formula for k-valued residues at a place with separable residue
field: Tr_{F_P/k} res_{P,s}(z) = Tr_{F_P/k} res_{P,t}(z · ds/dt).
The derivative dy/dt has residue zero with respect to t at a place with separable residue
field: the formal derivative of a Laurent series has no T⁻¹ term.
The derivative dy/dt has k-valued residue zero with respect to t.
The residue res_P(ω) ∈ F_P of a Kähler differential ω at a place with separable
residue field (Stichtenoth, Definition 4.2.10 and Remark 4.3.7): writing ω = z dt for a
separating uniformizer t at P, it is the residue res_{P,t}(z). It does not depend on t
(TauCeti.Place.kaehlerResidueResidueField_eq_kaehlerResidueResidueField).
Instances For
The residue of ω is the residue of its coordinate ω / dt in the basis dt.
The residue of z dt is res_{P,t}(z).
Exact differentials have residue zero: res_P(dy) = 0.
The residue of a differential at a place with separable residue field is well defined (Stichtenoth, Definition 4.2.10): it does not depend on the separating uniformizer used to compute it.
The k-valued residue Tr_{F_P/k} res_P(ω) of a Kähler differential ω at a place with
separable residue field (Stichtenoth, Remark 4.3.7). It does not depend on the separating
uniformizer t (TauCeti.Place.kaehlerTraceResidue_eq_kaehlerTraceResidue), and at a rational
place it is TauCeti.Place.kaehlerResidue (TauCeti.Place.kaehlerTraceResidue_eq_kaehlerResidue).
Instances For
The k-valued residue is the trace of the residue.
The k-valued residue of z dt is Tr_{F_P/k} res_{P,t}(z).
Exact differentials have k-valued residue zero.
The k-valued residue of a differential is well defined: it does not depend on the
separating uniformizer used to compute it.
At a rational place the k-valued residue of a differential is its residue
TauCeti.Place.kaehlerResidue.