The local components of dt at a zero of t - a are residues

Let F / k be an algebraic function field and t ∈ F a separating element, and let dt be the Weil differential TauCeti.weilDifferentialOfSeparating, the cotrace to F of the canonical differential η of k(t). At a place P of F whose residue field F_P is separable over k and at which t - a is a prime element for some constant a ∈ k, ord_P (t - a) = 1, the local component of dt is the trace residue in t - a:

(dt)_P (u) = Tr_{F_P/k} (res_{P,t-a} (u)) for every u ∈ F.

At a rational place the trace is the identity and this is the residue res_{P,t-a} (u). This is Stichtenoth's Theorem 4.3.2(d), (z · δ(x))_P (u) = res_P (u z dx), in its form for places of arbitrary degree (Remark 4.3.7(d)), for x = t with t - a a prime element at P and z = 1. It identifies the abstract local components of Weil differentials with the classical residues of Laurent expansions.

The proof transports the rational-function-field case (TauCeti.repartitionDualComponent_ratFuncWeilDifferential_adicOfIrreducible_X_sub_C) along the cotrace. The place P lies over the zero P_a of t - a in k(t) with e(P ∣ P_a) = 1, and dt is regular at every place over P_a because the different is effective. Weak approximation moves u, without changing its principal part at P, to a function that is regular at the other places over P_a; for such a function the local components of the cotrace over P_a (TauCeti.trace_finsum_repartitionDualComponent_weilDifferentialCotrace) give (dt)_P (u) = η_{P_a} (Tr u) = res_{P_a,t-a} (Tr u). Finally the residue of the trace is the trace residue (TauCeti.Place.residue_trace).

Main results

• repartitionDualComponent_weilDifferentialCotrace_ratFuncWeilDifferential_eq_traceResidue: for a finite separable extension F of k(t), the local component of the cotrace of η at a place with separable residue field where t - a is a prime element is Tr ∘ res_{P,t-a}.
• TauCeti.repartitionDualComponent_weilDifferentialOfSeparating_eq_traceResidue: (dt)_P = Tr ∘ res_{P,t-a}.
• TauCeti.repartitionDualComponent_weilDifferentialCotrace_ratFuncWeilDifferential and TauCeti.repartitionDualComponent_weilDifferentialOfSeparating: at a rational place, (dt)_P = res_{P,t-a}.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 4.3.2(d) and Remark 4.3.7(d).

The place below a place at which t - a is a prime element

theorem TauCeti.repartitionDualComponent_weilDifferentialCotrace_ratFuncWeilDifferential_eq_traceResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hF : IsFunctionField k F) {P : Place k F} [Algebra.IsSeparable k P.ResidueField] {a : k} (ht : P.ord ((algebraMap (RatFunc k) F) (RatFunc.X - RatFunc.C a)) = 1) (u : F) : (repartitionDualComponent (↑((weilDifferentialCotrace k F ⋯ hF) ⟨ratFuncWeilDifferential k, ⋯⟩)) P) u = (P.traceResidue ht) u

The local component of dt at a zero of t - a is the trace residue in t - a (Stichtenoth, Theorem 4.3.2(d) and Remark 4.3.7(d)): for a finite separable extension F of k(t) and a place P of F with residue field separable over k, at which the image of t - a is a prime element, the local component at P of the cotrace of the canonical differential η = dt of k(t) is Tr_{F_P/k} ∘ res_{P,t-a}.

theorem TauCeti.repartitionDualComponent_weilDifferentialCotrace_ratFuncWeilDifferential {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hF : IsFunctionField k F) {P : Place k F} (hP : P.degree = 1) {a : k} (ht : P.ord ((algebraMap (RatFunc k) F) (RatFunc.X - RatFunc.C a)) = 1) (u : F) : (repartitionDualComponent (↑((weilDifferentialCotrace k F ⋯ hF) ⟨ratFuncWeilDifferential k, ⋯⟩)) P) u = (P.residue hP ht) u

The local component of dt at a zero of t - a is the residue in t - a (Stichtenoth, Theorem 4.3.2(d)): for a finite separable extension F of k(t) and a rational place P of F at which the image of t - a is a prime element, the local component at P of the cotrace of the canonical differential η = dt of k(t) is res_{P,t-a}.

theorem TauCeti.repartitionDualComponent_weilDifferentialOfSeparating_eq_traceResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {t : F} (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] {P : Place k F} [Algebra.IsSeparable k P.ResidueField] {a : k} (ht : P.ord (t - (algebraMap k F) a) = 1) (u : F) : (repartitionDualComponent (↑(weilDifferentialOfSeparating hF htr)) P) u = (P.traceResidue ht) u

The local component of dt at a zero of t - a is the trace residue in t - a (Stichtenoth, Theorem 4.3.2(d) and Remark 4.3.7(d)): for a separating element t of F / k and a place P with residue field separable over k at which t - a is a prime element, the Weil differential dt has local component (dt)_P = Tr_{F_P/k} ∘ res_{P,t-a}.

theorem TauCeti.repartitionDualComponent_weilDifferentialOfSeparating {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {t : F} (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] {P : Place k F} (hP : P.degree = 1) {a : k} (ht : P.ord (t - (algebraMap k F) a) = 1) (u : F) : (repartitionDualComponent (↑(weilDifferentialOfSeparating hF htr)) P) u = (P.residue hP ht) u

The local component of dt at a zero of t - a is the residue in t - a (Stichtenoth, Theorem 4.3.2(d)): for a separating element t of F / k and a rational place P at which t - a is a prime element, the Weil differential dt has local component (dt)_P = res_{P,t-a}.