Nonspecial divisors of degree g on prescribed rational places

A divisor B of a function field F / k of genus g is nonspecial when its index of specialty i(B) = ℓ(B) - deg B - 1 + g vanishes. Every divisor of degree at least 2g - 1 is nonspecial, and an effective nonspecial divisor has degree at least g. This file shows that this smallest degree is attained on any prescribed set of at least g rational places:

if T is a set of places of degree one with at least g elements, then some effective divisor B with support in T has deg B = g and ℓ(B) = 1, equivalently i(B) = 0.

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.6.12, over an arbitrary exact constant field.

Main results

• TauCeti.Divisor.exists_degree_eq_genus_dim_eq_one: nonspecial divisors of degree g supported on any prescribed set of at least g rational places (Stichtenoth, Proposition 1.6.12).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 1.6.10 and Proposition 1.6.12.

theorem TauCeti.Divisor.exists_degree_eq_genus_dim_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {T : Set (Place k F)} (hT : ∀ P ∈ T, P.degree = 1) (hcard : ↑(genus k F) ≤ T.encard) : ∃ (B : Divisor k F), 0 ≤ B ∧ ↑B.support ⊆ T ∧ degree B = ↑(genus k F) ∧ B.dim = 1 ∧ B.indexOfSpecialty = 0

Nonspecial divisors of degree g on prescribed rational places (Stichtenoth, Proposition 1.6.12). Let F / k be a function field of genus g with exact constant field, and let T be a set of places of degree one with at least g elements. Then there is an effective divisor B supported in T with deg B = g and ℓ(B) = 1; equivalently, B is nonspecial, i(B) = 0.