Riemann--Roch in high degree

For a divisor D of a function field of genus g, the Riemann--Roch theorem simplifies to

ℓ(D) = deg D + 1 - g

as soon as deg D > 2g - 2. Indeed, if W is a canonical divisor, then W - D has negative degree, so its Riemann--Roch space vanishes. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 1.5.17.

The genus-one specialization gives the section-dimension ladder ℓ(nP) = n * deg P at every place P and every positive integer n; at a rational place it reads ℓ(nP) = n, the dimension input for the construction of Weierstrass coordinates.

Main results

• TauCeti.Divisor.dim_eq_degree_add_one_sub_genus_of_two_mul_genus_sub_one_le_degree: the high-degree form of Riemann--Roch.
• TauCeti.Divisor.indexOfSpecialty_eq_zero_of_two_mul_genus_sub_one_le_degree: divisors above the canonical degree are nonspecial.
• TauCeti.Divisor.dim_eq_degree_of_genus_eq_one: in genus one, every positive-degree divisor has dimension equal to its degree.
• TauCeti.Divisor.dim_natCast_zsmul_ofPoint_of_genus_eq_one: ℓ(nP) = n * deg P at a place of a genus-one function field, for n >= 1.
• TauCeti.Divisor.dim_single_of_genus_eq_one: ℓ(nP) = n at a rational place of a genus-one function field, for n >= 1.
• Place.exists_poles_eq_natCast_zsmul_ofPoint_of_two_mul_genus_sub_one_le_sub_one_mul_degree: a function with pole divisor exactly nP exists as soon as 2g - 1 <= (n - 1) * deg P.
• TauCeti.Place.exists_ord_eq_neg_and_forall_ne_ord_nonneg: for every n >= 2g, a nonzero function has order -n at a prescribed place and is regular elsewhere.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.5.17.

theorem TauCeti.Divisor.dim_eq_degree_add_one_sub_genus_of_two_mul_genus_sub_one_le_degree {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} (hD : 2 * ↑(genus k F) - 1 ≤ degree D) : ↑D.dim = degree D + 1 - ↑(genus k F)

Riemann--Roch in high degree (Stichtenoth, Theorem 1.5.17): if deg D >= 2g - 1, then

ℓ(D) = deg D + 1 - g.

The statement uses integers throughout, matching both divisor degree and the Riemann--Roch identity and avoiding a truncated natural-number subtraction.

theorem TauCeti.Divisor.indexOfSpecialty_eq_zero_of_two_mul_genus_sub_one_le_degree {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} (hD : 2 * ↑(genus k F) - 1 ≤ degree D) : D.indexOfSpecialty = 0

The weak-inequality spelling of nonspeciality in high degree: deg D >= 2g - 1 implies i(D) = 0.

Genus one

theorem TauCeti.Divisor.dim_eq_degree_of_genus_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) (hg : genus k F = 1) {D : Divisor k F} (hD : 0 < degree D) : ↑D.dim = degree D

On a genus-one function field, every divisor of positive degree has Riemann--Roch dimension equal to its degree.

theorem TauCeti.Divisor.dim_natCast_zsmul_ofPoint_of_genus_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) (hg : genus k F = 1) {P : Place k F} {n : ℕ} (hn : 1 ≤ n) : dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P) = n * P.degree

On a genus-one function field, the Riemann--Roch space of nP has dimension n * deg P for every place P and every positive natural number n.

This is the genus-one section-dimension ladder; at a rational place it reads ℓ(nP) = n, the dimension input used to construct Weierstrass coordinates.

theorem TauCeti.Divisor.dim_single_of_genus_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) (hg : genus k F = 1) {P : Place k F} (hP : P.degree = 1) {n : ℕ} (hn : 1 ≤ n) : dim (Finsupp.single P ↑n) = n

On a genus-one function field, the Riemann--Roch space of nP at a rational place has dimension n for every positive natural number n.

Functions with one prescribed pole

theorem TauCeti.Place.exists_ord_eq_neg_and_forall_ne_ord_nonneg_of_dim_lt {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (P : Place k F) {n : ℕ} (hdimlt : Divisor.dim (↑(n - 1) • AlgebraicGeometry.WeilDivisor.ofPoint P) < Divisor.dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P)) : ∃ (x : F), x ≠ 0 ∧ P.ord x = -↑n ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord x

If the Riemann--Roch dimensions of (n - 1)P and nP differ, there is a nonzero function with order exactly -n at P that is regular at every other place.

theorem TauCeti.Place.exists_ord_eq_neg_and_forall_ne_ord_nonneg_of_two_mul_genus_sub_one_le_sub_one_mul_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) {n : ℕ} (hnpos : 0 < n) (hn : 2 * ↑(genus k F) - 1 ≤ (↑n - 1) * ↑P.degree) : ∃ (x : F), x ≠ 0 ∧ P.ord x = -↑n ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord x

For every place P and every positive n with 2g - 1 <= (n - 1) * deg P, there is a nonzero function with a pole of order exactly n at P and no other poles (Stichtenoth, Proposition 1.6.6).

The hypothesis is exactly what makes (n - 1)P a high-degree divisor, so the consecutive Riemann--Roch spaces differ in dimension.

theorem TauCeti.Place.exists_ord_eq_neg_and_forall_ne_ord_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) {n : ℕ} (hn : 2 * genus k F ≤ n) : ∃ (x : F), x ≠ 0 ∧ P.ord x = -↑n ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord x

For every place P and natural number n >= 2g, there is a nonzero function with order -n at P that is regular at every other place (Stichtenoth, Proposition 1.6.6).

theorem TauCeti.Place.exists_poles_eq_natCast_zsmul_ofPoint_of_two_mul_genus_sub_one_le_sub_one_mul_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) {n : ℕ} (hnpos : 0 < n) (hn : 2 * ↑(genus k F) - 1 ≤ (↑n - 1) * ↑P.degree) : ∃ (z : Fˣ), Divisor.poles hF z = ↑n • AlgebraicGeometry.WeilDivisor.ofPoint P

For every place P and every positive n with 2g - 1 <= (n - 1) * deg P, some function has pole divisor exactly nP (Stichtenoth, Proposition 1.6.6).

theorem TauCeti.Place.exists_poles_eq_natCast_zsmul_ofPoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) {n : ℕ} (hn : 2 * genus k F ≤ n) : ∃ (z : Fˣ), Divisor.poles hF z = ↑n • AlgebraicGeometry.WeilDivisor.ofPoint P

For every place P and n >= 2g, some function has pole divisor exactly nP (Stichtenoth, Proposition 1.6.6).