theorem riemann_roch_line_bundle_p1 (k : Type) [Field k] (d : ℤ) : ↑(RiemannRoch.dimH0 k d) - ↑(RiemannRoch.dimH1 k d) = d + 1

Riemann–Roch for line bundles on ℙ¹: h⁰(O(d)) − h¹(O(d)) = d + 1.

theorem serre_duality_classical_P1 (k : Type) [Field k] (d : ℤ) : ↑(RiemannRoch.dimH0 k d) - ↑(RiemannRoch.dimH0 k (-2 - d)) = d + 1

Classical Serre form of Riemann–Roch on ℙ¹: h⁰(O(d)) − h⁰(O(K - d)) = d + 1, with K_{ℙ¹} of degree -2.

theorem genus_P1 (k : Type) [Field k] : RiemannRoch.dimH1 k 0 = 0

The genus of ℙ¹: h¹(O_{ℙ¹}) = 0.

theorem arithmetic_eq_geometric_genus_P1 (k : Type) [Field k] : RiemannRoch.dimH1 k 0 = RiemannRoch.dimH0 k (-2)

Arithmetic genus equals geometric genus on ℙ¹: both vanish.

theorem deg_canonical_P1 : -2 = 2 * 0 - 2

The degree of the canonical divisor on ℙ¹ equals 2g − 2 = -2.

theorem dimH0_ge_P1 (k : Type) [Field k] (d : ℤ) : ↑(RiemannRoch.dimH0 k d) ≥ d + 1 - 0

Riemann's inequality on ℙ¹: h⁰(O(d)) ≥ d + 1 − g_{ℙ¹} = d + 1.

theorem cech_duality_dimension_P1 (k : Type) [Field k] (n : ℤ) : RiemannRoch.dimH1 k n = RiemannRoch.dimH0 k (-2 - n)

Čech-level Serre duality on ℙ¹: dim H¹(O(n)) = dim H⁰(O(-2 - n)).