Trace residues of Weil differentials

Let F / k be an algebraic function field with exact constant field k. At a place P with separable residue field, choose a separating uniformizer t. Every Weil differential has a unique expression ω = z dt, since the Weil differential space is one-dimensional. Its local component at u is the residue-field trace of the coefficient of t⁻¹ in the Laurent expansion of z u.

Here z is obtained from the existing basis weilDifferentialBasisOfSeparating, rather than from a new differential carrier. The formula extends repartitionDualComponent_weilDifferentialOfSeparating_eq_traceResidue from dt to arbitrary Weil differentials, including at nonrational places. In particular, the trace residue is independent of the separating uniformizer, because it equals the intrinsic local component.

For a family of separating uniformizers, these trace residues have finite support on every repartition. Their sum on a diagonal function is zero. This is the residue theorem with residue-field traces; no algebraic closure or infinitude of the constant field is required. The hypotheses explicitly require separable residue fields and separating uniformizers, both available over a perfect constant field. Once F / k has a separating element, every uniformizer at a place with separable residue field is separating (TauCeti.Place.isSeparable_adjoin_of_ord_eq_one).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Theorem 4.3.2(d), Corollary 4.3.3 and Remark 4.3.7(d).

theorem TauCeti.repartitionDualComponent_eq_traceResidue_coord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {P : Place k F} [Algebra.IsSeparable k P.ResidueField] {t : F} (ht : P.ord t = 1) [Algebra.IsSeparable (↥k⟮t⟯) F] (ω : ↥(weilDifferentialSpace k F)) (u : F) : have htr := ⋯; (repartitionDualComponent (↑ω) P) u = (P.traceResidue ht) (((weilDifferentialBasisOfSeparating hF hex htr).coord ()) ω * u)

The local component of ω = z dt is the trace residue of z u, at a place of any degree with separable residue field and a separating uniformizer t. The coefficient z is the coordinate of ω in the basis dt.

theorem TauCeti.finite_support_traceResidue_coord {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) [∀ (P : Place k F), Algebra.IsSeparable k P.ResidueField] (t : Place k F → F) (ht : ∀ (P : Place k F), P.ord (t P) = 1) [∀ (P : Place k F), Algebra.IsSeparable (↥k⟮t P⟯) F] (ω : ↥(weilDifferentialSpace k F)) (a : ↥(repartitionSpace k F)) : have htr := ⋯; (Function.support fun (P : Place k F) => (P.traceResidue ⋯) (((weilDifferentialBasisOfSeparating hF hex ⋯).coord ()) ω * ↑a P)).Finite

The local trace residues of a Weil differential on a repartition are nonzero at only finitely many places, even when the places are not rational.

theorem TauCeti.finsum_traceResidue_coord_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) [∀ (P : Place k F), Algebra.IsSeparable k P.ResidueField] (t : Place k F → F) (ht : ∀ (P : Place k F), P.ord (t P) = 1) [∀ (P : Place k F), Algebra.IsSeparable (↥k⟮t P⟯) F] (ω : ↥(weilDifferentialSpace k F)) (u : F) : have htr := ⋯; ∑ᶠ (P : Place k F), (P.traceResidue ⋯) (((weilDifferentialBasisOfSeparating hF hex ⋯).coord ()) ω * u) = 0

The residue theorem with residue-field traces: if ω = z_P dt_P at each place, then ∑_P Tr(res_{P,t_P}(z_P u)) = 0 for every function u. The summands have finite support by finite_support_traceResidue_coord, applied to the constant repartition.