Clifford's theorem for divisors of a function field

This file proves Clifford's dimension bound for a divisor D of an algebraic function field over an arbitrary exact field of constants, assuming 0 ≤ deg D ≤ 2g - 2:

2 * ℓ(D) ≤ deg D + 2.

The main input is the dimension inequality

ℓ(A) + ℓ(B) ≤ 1 + ℓ(A + B)

when both Riemann–Roch spaces are nonzero. Its proof replaces A and B by effective representatives, chooses a divisor D₀ ≤ A of least degree with L(D₀) = L(A), and uses that a vector space over a field with more than m elements is not a union of m proper subspaces. A section of L(D₀) can therefore be chosen with the exact pole order prescribed by D₀ at every place in the support of B, as soon as the constant field has more than deg B + 1 elements. Multiplication by that section embeds L(B) / k into L(A + B) / L(A).

Over a finite constant field there may be too few constants for this choice. The inequality is then proved after a finite constant field extension F · k' / k' with enough constants: the conorm preserves degrees and the dimensions of Riemann–Roch spaces, and k' stays exact since finite fields are perfect.

Applying the inequality to A = D and B = W - D, for a canonical divisor W, and using Riemann--Roch gives Clifford's theorem. This is the route of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Lemma 1.6.14 and Theorem 1.6.13, whose choice of the section uses an infinite constant field; the reduction from a finite constant field uses the constant field extensions of Theorem 3.6.3.

Main results

• TauCeti.Divisor.dim_add_dim_le_one_add_dim_add_of_lt_card: Stichtenoth's dimension inequality ℓ(A) + ℓ(B) ≤ 1 + ℓ(A + B) when the constant field has more than deg B + 1 elements, in particular when it is infinite.
• TauCeti.Divisor.dim_add_dim_le_one_add_dim_add: the dimension inequality over an arbitrary exact constant field.
• TauCeti.Divisor.two_mul_dim_le_degree_add_two: Clifford's theorem over an arbitrary exact constant field.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Lemma 1.6.14, Theorem 1.6.13 and Theorem 3.6.3.

theorem TauCeti.Divisor.dim_add_dim_le_one_add_dim_add_of_lt_card {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {A B : Divisor k F} (hA : 0 < A.dim) (hB : 0 < B.dim) (hcard : ↑(degree B).toNat + 1 < ENat.card k) : A.dim + B.dim ≤ 1 + (A + B).dim

Stichtenoth, Lemma 1.6.14: if L(A) and L(B) are nonzero and the exact constant field has more than deg B + 1 elements, then

ℓ(A) + ℓ(B) ≤ 1 + ℓ(A + B).

The cardinality hypothesis holds for every infinite constant field.

theorem TauCeti.Divisor.dim_add_dim_le_one_add_dim_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {A B : Divisor k F} (hA : 0 < A.dim) (hB : 0 < B.dim) : A.dim + B.dim ≤ 1 + (A + B).dim

Stichtenoth, Lemma 1.6.14, over any exact constant field: if L(A) and L(B) are nonzero, then

ℓ(A) + ℓ(B) ≤ 1 + ℓ(A + B).

theorem TauCeti.Divisor.two_mul_dim_le_degree_add_two {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} (hDnonneg : 0 ≤ degree D) (hDle : degree D ≤ 2 * ↑(genus k F) - 2) : 2 * ↑D.dim ≤ degree D + 2

Clifford's theorem (Stichtenoth, Theorem 1.6.13), over an arbitrary exact field of constants: a divisor of degree between 0 and 2g - 2 satisfies

2 * ℓ(D) ≤ deg D + 2.

The bound includes the nonspecial and empty-linear-system edge cases.