The Riemann–Roch spaces and the genus of the rational function field

The rational function field k(x) is the base case of the theory, and its Riemann–Roch spaces can be written down by hand, long before the Riemann–Roch theorem is available. For n : ℕ, a rational function lies in L(n · P_∞) exactly when it is a polynomial of degree at most n: having no pole at any finite place makes it a polynomial, and ord_∞ f = -deg f turns the remaining condition into the degree bound. Hence

ℓ(n · P_∞) = n + 1 = deg (n · P_∞) + 1,

and comparing this with Riemann's theorem in large degree gives g(k(x)) = 0: the rational function field has genus zero, and Riemann's inequality ℓ(D) ≥ deg D + 1 - g is sharp at n · P_∞ for every n ≥ 0.

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Example 1.4.18 (with Proposition 1.4.9 for the description of L(n · P_∞)).

The polynomiality step is TauCeti.Place.forall_ord_adicOfIrreducible_nonneg_iff, which reads Mathlib's IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one for the Dedekind domain k[X] in place vocabulary. It combines with TauCeti.Place.eq_infty_or_exists_eq_ofPrime: the places of k(x) are the height-one primes of k[X] together with P_∞, so the two conditions defining L(n · P_∞) split exactly along that classification.

Main results

• TauCeti.mem_riemannRochSpace_zsmul_ofPoint_infty_iff and TauCeti.riemannRochSpace_zsmul_ofPoint_infty: L(n · P_∞) is the space of polynomials of degree at most n for n : ℕ, in membership form and as an equality of k-subspaces of k(x).
• TauCeti.Divisor.dim_natCast_zsmul_ofPoint_infty: ℓ(n · P_∞) = n + 1 for n : ℕ, the model computation of Example 1.4.18; TauCeti.Divisor.dim_zsmul_ofPoint_infty gives the formula for every integer, including negative multiples where the space is trivial.
• TauCeti.genus_ratFunc: the rational function field has genus zero.
• TauCeti.Divisor.degree_add_one_le_dim_ratFunc: Riemann's theorem on k(x), with the genus evaluated: ℓ(D) ≥ deg D + 1 for every divisor D of k(x).
• TauCeti.Divisor.linearlyEquivalent_zsmul_ofPoint_infty: every divisor of k(x) is linearly equivalent to (deg D) · P_∞, so a divisor class on the rational function field is determined by its degree; hence TauCeti.Divisor.dim_ratFunc, the closed formula ℓ(D) = (deg D + 1)⁺ for every divisor of k(x), not only the multiples of P_∞.
• TauCeti.Divisor.degreeZeroClassGroupEquivPolynomial: Cl⁰(k(x)) ≃+ ClassGroup k[X], the affine class-group bridge at the model k[X], whose only place at infinity is the rational place P_∞; hence TauCeti.Divisor.ker_degreeClass_ratFunc_eq_bot and TauCeti.Divisor.classNumber_ratFunc, the rational function field has class number one (Stichtenoth, Example 5.1).

Provenance

The mathematics is Stichtenoth's and the Lean development is independent, as in TauCeti.FieldTheory.FunctionField.RiemannRoch.Genus. The separate vaca22/riemann-roch-function-fields project (Guanghao Li, Apache-2.0) carries a complete function-field Riemann–Roch development by the same Stichtenoth route; no code is copied or adapted from it here.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Example 1.4.18.
• The polynomials of bounded degree and their basis of monomials are Mathlib/RingTheory/Polynomial/Basic.lean and Mathlib/RingTheory/Polynomial/DegreeLT.lean (Anne Baanen, Kenny Lau); the criterion for a fraction to be integral at every height-one prime is Mathlib/RingTheory/DedekindDomain/AdicValuation.lean (María Inés de Frutos-Fernández).

L(n · P_∞) is the space of polynomials of degree at most n

theorem TauCeti.mem_riemannRochSpace_zsmul_ofPoint_infty_iff {k : Type u_1} [Field k] {n : ℕ} {f : RatFunc k} : f ∈ riemannRochSpace (↑n • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) ↔ ∃ (q : Polynomial k), q.degree ≤ ↑n ∧ (algebraMap (Polynomial k) (RatFunc k)) q = f

The Riemann–Roch spaces of k(x) at infinity (Stichtenoth, Example 1.4.18): a rational function lies in L(n · P_∞) for n : ℕ exactly when it is a polynomial of degree at most n.

Regularity at the finite places is exactly polynomiality, by TauCeti.Place.forall_ord_adicOfIrreducible_nonneg_iff; the remaining condition at infinity is deg f ≤ n, because ord_∞ is minus the degree.

theorem TauCeti.riemannRochSpace_zsmul_ofPoint_infty (k : Type u_2) [Field k] (n : ℕ) : riemannRochSpace (↑n • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) = Submodule.map (IsScalarTower.toAlgHom k (Polynomial k) (RatFunc k)).toLinearMap (Polynomial.degreeLE k ↑n)

The Riemann–Roch spaces of k(x) at infinity, as an equality of k-subspaces of k(x): for n : ℕ, L(n · P_∞) is the image of the polynomials of degree at most n.

theorem TauCeti.Divisor.dim_natCast_zsmul_ofPoint_infty (k : Type u_2) [Field k] (n : ℕ) : dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) = n + 1

ℓ(n · P_∞) = n + 1 (Stichtenoth, Example 1.4.18): the polynomials of degree at most n form a k-space of dimension n + 1, with basis 1, x, …, xⁿ.

@[simp]

theorem TauCeti.Divisor.dim_zsmul_ofPoint_infty (k : Type u_2) [Field k] (n : ℤ) : dim (n • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) = (n + 1).toNat

ℓ(n · P_∞) for every integer n: it is n + 1 for n ≥ 0, and 0 once n < 0.

The genus is zero

@[simp]

theorem TauCeti.genus_ratFunc (k : Type u_2) [Field k] : genus k (RatFunc k) = 0

The rational function field has genus zero (Stichtenoth, Example 1.4.18).

Riemann's theorem gives a degree beyond which ℓ(D) = deg D + 1 - g; evaluating it at D = n · P_∞ for large n and comparing with ℓ(n · P_∞) = n + 1 = deg (n · P_∞) + 1 forces g = 0.

theorem TauCeti.Divisor.degree_add_one_le_dim_ratFunc {k : Type u_1} [Field k] (D : Divisor k (RatFunc k)) : degree D + 1 ≤ ↑D.dim

Riemann's theorem on k(x), with the genus evaluated: every divisor D of the rational function field satisfies ℓ(D) ≥ deg D + 1. Equality holds at D = n · P_∞ for n ≥ 0 by TauCeti.Divisor.dim_natCast_zsmul_ofPoint_infty, so Riemann's inequality is sharp on k(x).

Divisor classes on k(x)

theorem TauCeti.Divisor.linearlyEquivalent_zsmul_ofPoint_infty {k : Type u_1} [Field k] (D : Divisor k (RatFunc k)) : (Place.orderSystem ⋯).LinearlyEquivalent D (degree D • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k))

A divisor class on k(x) is determined by its degree: every divisor D of the rational function field is linearly equivalent to (deg D) · P_∞.

Since deg P_∞ = 1, the difference D - (deg D) · P_∞ has degree zero, and Riemann's theorem on k(x) gives it a nonzero Riemann–Roch space; a degree-zero divisor with a nonzero Riemann–Roch space is principal (Stichtenoth, Corollary 1.4.12(c)).

theorem TauCeti.Divisor.dim_ratFunc {k : Type u_1} [Field k] (D : Divisor k (RatFunc k)) : D.dim = (degree D + 1).toNat

ℓ(D) on the rational function field, for every divisor: ℓ(D) = (deg D + 1)⁺.

Every divisor of k(x) is linearly equivalent to (deg D) · P_∞, where the dimension was computed by hand in TauCeti.Divisor.dim_zsmul_ofPoint_infty. This is the Riemann–Roch answer on k(x), obtained without the Riemann–Roch theorem.

The class number of k(x)

noncomputable def TauCeti.Divisor.degreeZeroClassGroupEquivPolynomial (k : Type u_1) [Field k] : ↥(degreeClass ⋯).ker ≃+ Additive (ClassGroup (Polynomial k))

The degree-zero divisor class group of k(x) is the ideal class group of k[X]: the model k[X] has a single place at infinity (TauCeti.Place.exists_algebraMap_notMem_integers_iff_eq_infty), and that place is rational, so the affine bridge TauCeti.Divisor.degreeZeroClassGroupEquiv applies.

Equations

• TauCeti.Divisor.degreeZeroClassGroupEquivPolynomial k = TauCeti.Divisor.degreeZeroClassGroupEquiv (Polynomial k) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.Divisor.degreeZeroClassGroupEquivPolynomial_apply (k : Type u_1) [Field k] (c : ↥(degreeClass ⋯).ker) : (degreeZeroClassGroupEquivPolynomial k) c = (classGroupHom (Polynomial k) ⋯) ↑c

@[simp]

theorem TauCeti.Divisor.ker_degreeClass_ratFunc_eq_bot (k : Type u_1) [Field k] : (degreeClass ⋯).ker = ⊥

Every degree-zero divisor class of the rational function field is trivial: through the affine bridge it is an ideal class of k[X], and k[X] is a principal ideal domain. The description of the divisor classes of k(x) in TauCeti.Divisor.linearlyEquivalent_zsmul_ofPoint_infty gives the same conclusion directly.

@[simp]

theorem TauCeti.Divisor.classNumber_ratFunc (k : Type u_1) [Field k] : classNumber ⋯ = 1

The rational function field has class number one (Stichtenoth, Example 5.1).