Nonvanishing of local components of Weil differentials

Every local component of a nonzero Weil differential on an algebraic function field with exact constants is nonzero. Consequently, fixing any one place P, the map ω ↦ ω_P is injective on the space of Weil differentials: one local component determines the global differential.

The key point is that allowing a double pole at P strictly enlarges the space of regular Weil differentials. Indeed,

dim_k Ω_F(-2P) = 2 deg P - 1 + g > g = dim_k Ω_F(0).

Thus some differential in Ω_F(-2P) is not regular. Its local component at P cannot vanish, because the local-component characterization of the filtration would then make it regular after all. Since the full space of Weil differentials is one-dimensional over F, multiplication by a function carries this witness to any prescribed nonzero differential, and multiplication cannot create a zero local component.

This is the nonvanishing assertion and the final clause of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.7.3(a). It is the local input for defining the order of a Weil differential and for comparing Weil differentials with Kähler differentials through residues.

Main results

• TauCeti.repartitionDualComponent_ne_zero: over an exact constant field, every local component of a nonzero Weil differential is nonzero.
• TauCeti.repartitionDualComponent_eq_zero_iff: over an exact constant field, a Weil differential is zero exactly when its local component at one fixed place is zero.
• TauCeti.repartitionDualComponent_inj: over an exact constant field, two Weil differentials are equal exactly when their local components at one fixed place are equal.

References

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

theorem TauCeti.repartitionDualComponent_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)} (hω : ω ∈ weilDifferentialSpace k F) (hω0 : ω ≠ 0) (P : Place k F) : repartitionDualComponent ω P ≠ 0

Over an exact constant field, every local component of a nonzero Weil differential is nonzero (Stichtenoth, Proposition 1.7.3(a)).

@[simp]

theorem TauCeti.repartitionDualComponent_eq_zero_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)} (hω : ω ∈ weilDifferentialSpace k F) (P : Place k F) : repartitionDualComponent ω P = 0 ↔ ω = 0

Over an exact constant field, a Weil differential is zero exactly when its local component at one fixed place is zero.

@[simp]

theorem TauCeti.repartitionDualComponent_inj {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)} (hω : ω ∈ weilDifferentialSpace k F) (hη : η ∈ weilDifferentialSpace k F) (P : Place k F) : repartitionDualComponent ω P = repartitionDualComponent η P ↔ ω = η

Over an exact constant field, one local component determines a Weil differential: two Weil differentials are equal if and only if their local components at any one fixed place are equal.