theorem RiemannRochSpace.riemann_inequality {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (D : CurveDivisor C) : 0 ≤ indexOfSpeciality D

Riemann's inequality: the index of speciality of any divisor $D$ is nonnegative, i.e. $\dim L(D) \ge \deg D + 1 - g$.

theorem RiemannRochSpace.effective_of_mem_riemannRochSpace {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (D : CurveDivisor C) (f : Fˣ) (hf : ↑f ∈ riemannRochSpace D) : (CurveWithOrd.principalDivisor f + D).IsEffective

Membership in the Riemann–Roch space: if a unit $f \in F^\times$ lies in $L(D)$, then the divisor $(f) + D$ is effective.

theorem RiemannRochSpace.exists_nonzero_of_divisorDim_pos {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (D : CurveDivisor C) (h : 1 ≤ divisorDim D) : ∃ (f : Fˣ), ↑f ∈ riemannRochSpace D

If $\dim L(D) \ge 1$, then the Riemann–Roch space contains a nonzero element (chosen here as a unit of $F$).

theorem RiemannRochSpace.indexOfSpeciality_eq_of_linearlyEquivalent {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (A B : CurveDivisor C) (h : PicardGroup.LinearlyEquivalent (CurveDivisor C) CurveWithOrd.principalDivisors A B) : indexOfSpeciality A = indexOfSpeciality B

Linearly equivalent divisors have the same index of speciality. Both the degree and the Riemann–Roch dimension are invariant under linear equivalence.

theorem RiemannRochSpace.riemann_equality_large_degree {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] : ∃ (c : ℤ), ∀ (D : CurveDivisor C), (CurveDivisor.degree C) D ≥ c → indexOfSpeciality D = 0

For divisors of sufficiently large degree, the index of speciality vanishes: there exists a constant $c$ such that every divisor with $\deg D \ge c$ satisfies $\dim L(D) = \deg D + 1 - g$. The proof picks a maximizing divisor $A$ realizing the genus, then transfers the bound to any $D$ by linear equivalence after using $D - A$ to find an effective shift.

theorem RiemannRochSpace.riemann_theorem {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] : (∀ (D : CurveDivisor C), 0 ≤ indexOfSpeciality D) ∧ ∃ (c : ℤ), ∀ (D : CurveDivisor C), (CurveDivisor.degree C) D ≥ c → indexOfSpeciality D = 0

Riemann's theorem: the index of speciality is always nonnegative and vanishes for divisors of sufficiently large degree. Equivalently, $\dim L(D) \ge \deg D + 1 - g$ for all $D$, with equality for $\deg D \gg 0$.