The order of a Weil differential is a local invariant

The divisor (ω) of a nonzero Weil differential of an algebraic function field F / k with exact constant field is the greatest divisor D with ω ∈ Ω_F(D), a condition on all the places at once. Its coefficient v_P (ω) at a single place is nevertheless determined by the local component ω_P alone:

v_P (ω) = max {m : ℤ | ω_P z = 0 whenever v_P z ≤ exp m}.

That the maximum is attained by v_P (ω) is the bound ω ∈ Ω_F ((ω)) read at P; that nothing larger belongs to the set is the maximality of (ω), applied to the divisor obtained from (ω) by resetting its coefficient at P to m — the other coefficients are unchanged, so the local-component criterion for membership in Ω_F needs only the hypothesis at P.

This is the half of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.7.3(a) that mentions the divisor (ω); the other half, that ω_P never vanishes identically, is in TauCeti.FieldTheory.FunctionField.Differential.LocalNonvanishing.

At a rational place the characterization sharpens to a single value: writing r = v_P (ω), some function with a pole of order at most r + 1 at P is not killed by ω_P, and subtracting a constant multiple of t ^ (-r - 1) from it — possible because the residue field is k — lands in the part ω_P does kill. So ω_P is already nonzero on the single power t ^ (-r - 1) of any uniformizer t. This is what pins down the normalization of the canonical Weil differential of the rational function field.

Main results

• TauCeti.isGreatest_weilDifferentialOrder and TauCeti.le_weilDifferentialOrder_iff: the order v_P (ω) is the largest bound the local component ω_P respects (Stichtenoth, Proposition 1.7.3(a)).
• TauCeti.repartitionDualComponent_uniformizer_zpow_ne_zero: at a rational place, ω_P is nonzero on t ^ (-v_P (ω) - 1) for every uniformizer t.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.7.3(a).

theorem TauCeti.isGreatest_weilDifferentialOrder {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (P : Place k F) : IsGreatest {m : ℤ | ∀ (z : F), P.valuation z ≤ WithZero.exp m → (repartitionDualComponent ω P) z = 0} (weilDifferentialOrder hF hex hmem hω P)

The order of a nonzero Weil differential at a place is determined by its local component there (Stichtenoth, Proposition 1.7.3(a)): v_P (ω) is the greatest m for which ω_P kills every function whose pole at P is bounded by m.

theorem TauCeti.le_weilDifferentialOrder_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (P : Place k F) (m : ℤ) : m ≤ weilDifferentialOrder hF hex hmem hω P ↔ ∀ (z : F), P.valuation z ≤ WithZero.exp m → (repartitionDualComponent ω P) z = 0

The order of a nonzero Weil differential, as a bound on its local component (Stichtenoth, Proposition 1.7.3(a)): m ≤ v_P (ω) exactly when ω_P kills every function whose pole at P is bounded by m.

theorem TauCeti.repartitionDualComponent_uniformizer_zpow_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) {P : Place k F} (hdeg : P.degree = 1) {t : F} (ht : P.valuation.IsUniformizer t) : (repartitionDualComponent ω P) (t ^ (-weilDifferentialOrder hF hex hmem hω P - 1)) ≠ 0

At a rational place the order of a nonzero Weil differential is attained on a power of any uniformizer: with r = v_P (ω) and t a uniformizer at P, the local component ω_P does not kill t ^ (-r - 1).

So at a rational place a single power of a uniformizer already detects the order, which is what lets a normalization prescribe one value of one local component.