Upper bounds for the genus, and Riemann's inequality

Let F / k be an algebraic function field with exact constant field k, and let F₀ ⊆ F be a subfield containing k over which F is finite, of degree n. If a basis z₁, …, zₙ of F / F₀ lies in the Riemann–Roch space L(C) of a divisor C of F, then

g(F) ≤ 1 + n (g(F₀) - 1) + deg C.

The proof counts sections. For a divisor A of F₀, the products u zᵢ of a k-basis u of L(A) with the zᵢ are k-linearly independent, because the zᵢ are linearly independent over F₀; and they lie in L(Con A + C). Hence n ℓ(A) ≤ ℓ(Con A + C). The conorm multiplies degrees by n, Riemann's theorem bounds ℓ(A) below by deg A + 1 - g(F₀), and Riemann–Roch evaluates ℓ(Con A + C) as n deg A + deg C + 1 - g(F) once deg A is large; comparing the two gives the bound. The section count is the case k' = k of TauCeti.Divisor.card_mul_dim_le_finrank_mul_dim_conorm_add in TauCeti.FieldTheory.FunctionField.RiemannRoch.Conorm.

For F₀ = k(x) and F = k(x, y), the powers 1, y, …, y^{m - 1} with m = [F : k(x)] form a basis of F / k(x) lying in L((m - 1) (y)_∞), a divisor of degree (m - 1) [F : k(y)]. Since k(x) has genus zero, this is Riemann's inequality

g(F) ≤ ([F : k(x)] - 1) ([F : k(y)] - 1).

Neither statement needs k to be perfect or the extensions to be separable: only the constant field of F has to be exact, which is what makes Riemann–Roch an equality in large degree. The subfield F₀ need not have exact constants, since only Riemann's lower bound ℓ(A) ≥ deg A + 1 - g(F₀) is used there.

Main results

• TauCeti.genus_le_one_add_finrank_mul_genus_sub_one_add_degree: g(F) ≤ 1 + [F : F₀] (g(F₀) - 1) + deg C for a basis of F / F₀ in L(C).
• TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one: Riemann's inequality g ≤ ([F : k(x)] - 1) ([F : k(y)] - 1) for F = k(x, y).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.11, Corollary 3.11.4.

theorem TauCeti.genus_le_one_add_finrank_mul_genus_sub_one_add_degree {k : Type u_1} {F₀ : Type u_2} {F : Type u_3} [Field k] [Field F₀] [Field F] [Algebra k F₀] [Algebra k F] [Algebra F₀ F] [IsScalarTower k F₀ F] [FiniteDimensional F₀ F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ι : Type u_4} (b : Module.Basis ι F₀ F) {C : Divisor k F} (hb : ∀ (i : ι), b i ∈ riemannRochSpace C) : ↑(genus k F) ≤ 1 + ↑(Module.finrank F₀ F) * (↑(genus k F₀) - 1) + Divisor.degree C

An upper bound for the genus from a subfield: if F / k has exact constants, F₀ is a subfield over which F is finite, and a basis of F / F₀ lies in L(C), then g(F) ≤ 1 + [F : F₀] (g(F₀) - 1) + deg C.

No hypothesis is placed on the constants of F₀: only Riemann's lower bound for ℓ on F₀ enters.

theorem TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one {k : Type u_1} {F : Type u_3} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x y : F} (hx : Transcendental k x) (hy : Transcendental k y) (hxy : k⟮x, y⟯ = ⊤) : genus k F ≤ (Module.finrank (↥k⟮x⟯) F - 1) * (Module.finrank (↥k⟮y⟯) F - 1)

Riemann's inequality (Stichtenoth, Corollary 3.11.4): if F / k has exact constants and is generated by two transcendental elements x and y, then g ≤ ([F : k(x)] - 1) ([F : k(y)] - 1).

The powers 1, y, …, y^{m - 1}, m = [F : k(x)], are a basis of F / k(x) in L((m - 1) (y)_∞), so this is the case F₀ = k(x) of TauCeti.genus_le_one_add_finrank_mul_genus_sub_one_add_degree.