The local components of dx on k(x) are residues

Let η be the canonical Weil differential of the rational function field k(x), the differential classically written dx (TauCeti.ratFuncWeilDifferential). At every rational place its local component is a residue of a Laurent expansion:

• at the place P_a of x - a, with the uniformizer x - a, η_{P_a} (z) = res_{P_a, x - a} (z);
• at the place at infinity, with the uniformizer x⁻¹, η_{P_∞} (z) = -res_{P_∞, x⁻¹} (x² z).

These are the two faces of η_P (z) = res_P (z dx): dx = d(x - a), while dx = -x² d(x⁻¹). This is the rational-function-field case of Stichtenoth's identification of local components with residues, and the base case from which it is transported to a separable extension of k(x) along the cotrace.

Feeding the identification back into the abstract residue theorem gives the residue theorem for k(x): if every pole of z is a rational place, then ∑_{a ∈ k} res_{P_a, x - a} (z) = res_{P_∞, x⁻¹} (x² z), the classical statement that the residues of z dx over ℙ¹(k) sum to zero. Over an algebraically closed field every place is rational, and the hypothesis disappears.

Main results

• TauCeti.repartitionDualComponent_ratFuncWeilDifferential_infty: η_{P_∞} (z) = -res_{P_∞, x⁻¹} (x² z).
• TauCeti.repartitionDualComponent_ratFuncWeilDifferential_adicOfIrreducible_X_sub_C: η_{P_a} (z) = res_{P_a, x - a} (z).
• TauCeti.finsum_residue_adicOfIrreducible_X_sub_C: the residue theorem for a rational function whose poles are rational places.
• TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed: the residue theorem for k(x) over an algebraically closed field.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.7.4, Theorem 4.3.2(d) and Corollary 4.3.3.

The local component at infinity

theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_infty {k : Type u_1} [Field k] (z : RatFunc k) : (repartitionDualComponent (ratFuncWeilDifferential k) (Place.infty k)) z = -((Place.infty k).residue ⋯ ⋯) (RatFunc.X ^ 2 * z)

The local component of dx at infinity is a residue (Stichtenoth, Theorem 4.3.2(d), for k(x)): η_{P_∞} (z) = -res_{P_∞, x⁻¹} (x² z), which is res_{P_∞} (z dx) since dx = -x² d(x⁻¹).

The local components at the finite rational places

theorem TauCeti.repartitionDualComponent_ratFuncWeilDifferential_adicOfIrreducible_X_sub_C {k : Type u_1} [Field k] (a : k) (z : RatFunc k) : (repartitionDualComponent (ratFuncWeilDifferential k) (Place.adicOfIrreducible ⋯)) z = ((Place.adicOfIrreducible ⋯).residue ⋯ ⋯) z

The local component of dx at the place of x - a is a residue (Stichtenoth, Theorem 4.3.2(d), for k(x)): η_{P_a} (z) = res_{P_a, x - a} (z), which is res_{P_a} (z dx) since dx = d(x - a).

The residue theorem

theorem TauCeti.finsum_residue_adicOfIrreducible_X_sub_C {k : Type u_1} [Field k] {z : RatFunc k} (hz : ∀ (P : Place k (RatFunc k)), P.degree ≠ 1 → z ∈ P.integers) : ∑ᶠ (a : k), ((Place.adicOfIrreducible ⋯).residue ⋯ ⋯) z = ((Place.infty k).residue ⋯ ⋯) (RatFunc.X ^ 2 * z)

The residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x)): if every pole of z is a rational place, then the residues of z dx over ℙ¹(k) sum to zero, in the form ∑_{a ∈ k} res_{P_a, x - a} (z) = res_{P_∞, x⁻¹} (x² z).

The hypothesis is needed: over ℚ, z = 2x / (x² - 2) is integral at every place P_a, so the left side vanishes, while res_{P_∞, x⁻¹} (x² z) = 2; the missing residue sits at the place of x² - 2, which has degree two.

theorem TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed {k : Type u_1} [Field k] [IsAlgClosed k] (z : RatFunc k) : ∑ᶠ (a : k), ((Place.adicOfIrreducible ⋯).residue ⋯ ⋯) z = ((Place.infty k).residue ⋯ ⋯) (RatFunc.X ^ 2 * z)

The residue theorem for k(x) over an algebraically closed field (Stichtenoth, Corollary 4.3.3, for k(x)): ∑_{a ∈ k} res_{P_a, x - a} (z) = res_{P_∞, x⁻¹} (x² z) for every rational function z.