The dimension of the space of Weil differentials

For an algebraic function field F / k with exact constant field this file computes the two dimensions of the space of Weil differentials, Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Lemma 1.5.7 and Proposition 1.5.9:

dim_k Ω_F(D) = i(D) and dim_F Ω_F = 1.

The first is formal. By construction Ω_F(D) is the annihilator of A_F(D) + F in the dual of A_F, so Submodule.dualQuotEquivDualAnnihilator identifies it with the dual of the cokernel A_F ⧸ (A_F(D) + F), whose dimension is the index of specialty (TauCeti.finrank_quotient_repartitionSpace). In particular Ω_F ≠ 0, because a divisor of degree at most -2 is special.

The second is the theorem with content. Suppose ω₁ and ω₂ are Weil differentials, bounded by D₁ and D₂, with ω₂ not a function multiple of ω₁. For x ∈ L(Dᵢ + B) the differential x · ωᵢ is bounded by -B, and the resulting k-linear map L(D₁ + B) × L(D₂ + B) → Ω_F(-B) is injective, so

ℓ(D₁ + B) + ℓ(D₂ + B) ≤ dim_k Ω_F(-B) = i(-B) = deg B - 1 + g

for every B > 0, while Riemann's theorem bounds the left-hand side below by 2 · deg B + deg D₁ + deg D₂ + 2 - 2g. Divisors of arbitrarily large degree exist, so for B large the two bounds collide and no such ω₂ exists.

Main results

• TauCeti.finrank_weilDifferentialFiltration: Stichtenoth, Lemma 1.5.7, dim_k Ω_F(D) = i(D), together with TauCeti.finiteDimensional_weilDifferentialFiltration.
• TauCeti.finrank_weilDifferentialFiltration_zero: dim_k Ω_F(0) = g (Remark 1.5.12).
• TauCeti.weilDifferentialSpace_ne_bot: there is a nonzero Weil differential.
• TauCeti.exists_repartitionDualMul_eq: every Weil differential is a function multiple of a fixed nonzero one.
• TauCeti.finrank_weilDifferentialSpace: Stichtenoth, Proposition 1.5.9, dim_F Ω_F = 1.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5.

dim_k Ω_F(D) = i(D)

theorem TauCeti.finiteDimensional_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) : FiniteDimensional k ↥(weilDifferentialFiltration D)

The Weil differentials bounded by a divisor form a finite-dimensional k-space: they are the dual of the finite-dimensional cokernel A_F ⧸ (A_F(D) + F).

theorem TauCeti.finrank_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (D : Divisor k F) : ↑(Module.finrank k ↥(weilDifferentialFiltration D)) = D.indexOfSpecialty

Stichtenoth, Lemma 1.5.7: dim_k Ω_F(D) = i(D). The Weil differentials bounded by D are the annihilator of A_F(D) + F, hence the dual of the cokernel A_F ⧸ (A_F(D) + F), whose dimension is the index of specialty.

theorem TauCeti.finrank_weilDifferentialFiltration_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.finrank k ↥(weilDifferentialFiltration 0) = genus k F

Stichtenoth, Remark 1.5.12: the regular Weil differentials, those bounded by the zero divisor, form a k-space of dimension the genus.

theorem TauCeti.weilDifferentialFiltration_eq_bot_iff_indexOfSpecialty_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) (D : Divisor k F) : weilDifferentialFiltration D = ⊥ ↔ D.indexOfSpecialty = 0

The divisors bounding no nonzero Weil differential are exactly the nonspecial ones.

theorem TauCeti.weilDifferentialSpace_ne_bot {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : weilDifferentialSpace k F ≠ ⊥

Stichtenoth, Lemma 1.5.7, in the form that gets used: an algebraic function field has a nonzero Weil differential. A strictly positive divisor B of degree at least 2 has i(-B) = deg B - 1 + g > 0, so Ω_F(-B) is already nonzero.

dim_F Ω_F = 1

theorem TauCeti.repartitionDualMul_mem_weilDifferentialFiltration_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {ω : Module.Dual k ↥(repartitionSpace k F)} {D B : Divisor k F} (hω : ω ∈ weilDifferentialFiltration D) {x : F} (hx : x ∈ riemannRochSpace (D + B)) : ((repartitionDualMul hF) x) ω ∈ weilDifferentialFiltration (-B)

Multiplying a Weil differential into a prescribed step of the filtration: if ω is bounded by D and the function x lies in L(D + B), then x · ω is bounded by -B.

theorem TauCeti.exists_repartitionDualMul_eq {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) (h₂ : ω₂ ∈ weilDifferentialSpace k F) : ∃ (c : F), ((repartitionDualMul hF) c) ω₁ = ω₂

Stichtenoth, Proposition 1.5.9, in element form: every Weil differential is a function multiple of any fixed nonzero one.

theorem TauCeti.finrank_weilDifferentialSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : Module.finrank F ↥(weilDifferentialSpace k F) = 1

Stichtenoth, Proposition 1.5.9: the Weil differentials of an algebraic function field with exact constant field form a one-dimensional vector space over the function field itself.