Uniqueness of the Riemann–Roch data

The Riemann–Roch theorem asserts that there are a natural number g₀ and a divisor W of an algebraic function field F / k with

ℓ(D) = deg D + 1 - g₀ + ℓ(W - D) for every divisor D.

This file proves that such a pair is essentially unique, before any such pair is constructed: g₀ is forced to be the genus g(F/k) of Riemann's theorem, W is forced to have ℓ(W) = g and deg W = 2g - 2, and any two such W are linearly equivalent, so they span a single divisor class. Once a Weil differential produces one such W — the canonical divisor — these statements say that the genus and the canonical class of the Riemann–Roch theorem are the genus and the canonical class, and not merely some pair that happens to satisfy the identity. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed. (GTM 254), Proposition 1.6.1.

The proofs use only Riemann's theorem and the degree-zero calculus already available: g₀ = g comes from evaluating the identity at divisors of large degree, where Riemann's theorem is an equality and ℓ(W - D) vanishes because W - D is a negative divisor; ℓ(W) = g₀ and deg W = 2g₀ - 2 come from evaluating it at D = 0 and at D = W; and the linear equivalence of two Riemann–Roch divisors comes from ℓ(W' - W) = 1 together with deg (W' - W) = 0, which is exactly the criterion for a degree-zero divisor to be principal.

The predicate is not vacuous: the rational function field satisfies the Riemann–Roch identity with g₀ = 0 and W = -2 · P_∞, proved here from the closed formula ℓ(D) = (deg D + 1)⁺ for divisors of k(x). Applying TauCeti.Divisor.IsRiemannRochDivisor's consequences to that witness recovers g(k(x)) = 0, ℓ(-2 · P_∞) = 0 and deg (-2 · P_∞) = -2 = 2g - 2.

Main definitions

• TauCeti.Divisor.IsRiemannRochDivisor: W satisfies the Riemann–Roch identity with the natural number g₀ in the role of the genus. The name is provisional in the sense that the results below show the only such divisors are the canonical ones, with g₀ = g.

Main results

• TauCeti.Divisor.IsRiemannRochDivisor.genus_eq: g₀ is the genus (Stichtenoth, Proposition 1.6.1).
• TauCeti.Divisor.IsRiemannRochDivisor.dim_eq and TauCeti.Divisor.IsRiemannRochDivisor.degree_eq: ℓ(W) = g₀ and deg W = 2g₀ - 2.
• TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq: the identity read as duality, i(D) = ℓ(W - D).
• TauCeti.Divisor.IsRiemannRochDivisor.linearlyEquivalent: any two Riemann–Roch divisors are linearly equivalent, so the class they determine — the canonical class — is well defined ahead of its construction; TauCeti.Divisor.IsRiemannRochDivisor.of_linearlyEquivalent is the converse transport, so the property depends only on the divisor class.
• TauCeti.Divisor.isRiemannRochDivisor_neg_two_zsmul_ofPoint_infty: -2 · P_∞ is a Riemann–Roch divisor of the rational function field, with g₀ = 0.

Provenance

The mathematics is Stichtenoth's and the Lean development is independent. 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, Proposition 1.6.1.

def TauCeti.Divisor.IsRiemannRochDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (W : Divisor k F) (g₀ : ℕ) : Prop

A Riemann–Roch divisor for the value g₀: a divisor W for which the Riemann–Roch identity ℓ(D) = deg D + 1 - g₀ + ℓ(W - D) holds at every divisor D, with the natural number g₀ in the role of the genus (Stichtenoth, Theorem 1.5.15 in the form of Proposition 1.6.1).

The results in this file show that g₀ is then the genus of F / k and that any two such W are linearly equivalent; the Riemann–Roch theorem itself is the assertion that one exists, and exhibits the divisor of a nonzero Weil differential as such a W.

Equations

• W.IsRiemannRochDivisor g₀ = ∀ (D : TauCeti.Divisor k F), ↑D.dim = TauCeti.Divisor.degree D + 1 - ↑g₀ + ↑(W - D).dim

theorem TauCeti.Divisor.isRiemannRochDivisor_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W : Divisor k F} {g₀ : ℕ} : W.IsRiemannRochDivisor g₀ ↔ ∀ (D : Divisor k F), ↑D.dim = degree D + 1 - ↑g₀ + ↑(W - D).dim

The defining property of a Riemann–Roch divisor, as an Iff for rewriting.

theorem TauCeti.Divisor.IsRiemannRochDivisor.dim_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W : Divisor k F} {g₀ : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hW : W.IsRiemannRochDivisor g₀) : W.dim = g₀

ℓ(W) = g₀ for a Riemann–Roch divisor (Stichtenoth, Corollary 1.5.16): evaluate the Riemann–Roch identity at D = 0, where ℓ(0) = 1.

theorem TauCeti.Divisor.IsRiemannRochDivisor.degree_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W : Divisor k F} {g₀ : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hW : W.IsRiemannRochDivisor g₀) : degree W = 2 * ↑g₀ - 2

deg W = 2g₀ - 2 for a Riemann–Roch divisor (Stichtenoth, Corollary 1.5.16): evaluate the Riemann–Roch identity at D = W, where ℓ(W - W) = ℓ(0) = 1, and use ℓ(W) = g₀.

theorem TauCeti.Divisor.IsRiemannRochDivisor.genus_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W : Divisor k F} {g₀ : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hW : W.IsRiemannRochDivisor g₀) : g₀ = genus k F

The value g₀ of a Riemann–Roch divisor is the genus (Stichtenoth, Proposition 1.6.1).

Riemann's theorem is an equality ℓ(D) = deg D + 1 - g in large degree. The divisors D = W + n · P, for a place P and n ≥ 1, have arbitrarily large degree and satisfy W - D = -n · P < 0, so ℓ(W - D) = 0 and the Riemann–Roch identity reads ℓ(D) = deg D + 1 - g₀ there; comparing the two forces g₀ = g.

theorem TauCeti.Divisor.IsRiemannRochDivisor.indexOfSpecialty_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W : Divisor k F} {g₀ : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hW : W.IsRiemannRochDivisor g₀) (D : Divisor k F) : D.indexOfSpecialty = ↑(W - D).dim

The Riemann–Roch identity, read as duality: for a Riemann–Roch divisor W, the index of specialty of D is ℓ(W - D) (Stichtenoth, Theorem 1.5.14 in the presence of Theorem 1.5.15).

theorem TauCeti.Divisor.IsRiemannRochDivisor.linearlyEquivalent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W W' : Divisor k F} {g₀ g₁ : ℕ} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hW : W.IsRiemannRochDivisor g₀) (hW' : W'.IsRiemannRochDivisor g₁) : (Place.orderSystem hF).LinearlyEquivalent W W'

Any two Riemann–Roch divisors are linearly equivalent (Stichtenoth, Proposition 1.6.1): they determine a single divisor class, the canonical class, and they do so before any of them has been constructed.

Both identities compute ℓ(W' - D) - ℓ(W - D) as a difference of the two values of g₀, which agree by TauCeti.Divisor.IsRiemannRochDivisor.genus_eq; taking D = W gives ℓ(W' - W) = 1, while deg (W' - W) = 0 by TauCeti.Divisor.IsRiemannRochDivisor.degree_eq, and a degree-zero divisor with a nonzero Riemann–Roch space is principal.

theorem TauCeti.Divisor.IsRiemannRochDivisor.of_linearlyEquivalent {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {W W' : Divisor k F} {g₀ : ℕ} (hF : IsFunctionField k F) (hW : W.IsRiemannRochDivisor g₀) (h : (Place.orderSystem hF).LinearlyEquivalent W W') : W'.IsRiemannRochDivisor g₀

Being a Riemann–Roch divisor depends only on the divisor class: linearly equivalent divisors have Riemann–Roch spaces of the same dimension, so the identity transports.

The rational function field

theorem TauCeti.Divisor.isRiemannRochDivisor_neg_two_zsmul_ofPoint_infty (k : Type u_3) [Field k] : IsRiemannRochDivisor (-2 • AlgebraicGeometry.WeilDivisor.ofPoint (Place.infty k)) 0

-2 · P_∞ is a Riemann–Roch divisor of k(x), with g₀ = 0: the closed formula ℓ(D) = (deg D + 1)⁺ on the rational function field turns the Riemann–Roch identity into an identity between truncated integers.

This is the witness that keeps TauCeti.Divisor.IsRiemannRochDivisor from being vacuous, and the acceptance instance for the general statements above: it has deg (-2 · P_∞) = -2, ℓ(-2 · P_∞) = 0 and, by TauCeti.Divisor.IsRiemannRochDivisor.genus_eq, g(k(x)) = 0.