noncomputable def RiemannRoch.dimH0 (k : Type) [Field k] (n : ℤ) : ℕ

Dimension of H^0(ℙ¹, 𝒪(n)) over k, via the Čech computation.

noncomputable def RiemannRoch.dimH1 (k : Type) [Field k] (n : ℤ) : ℕ

Dimension of H^1(ℙ¹, 𝒪(n)) over k, via the Čech computation.

theorem RiemannRoch.dimH0_nonneg (k : Type) [Field k] (m : ℕ) : dimH0 k ↑m = m + 1

On ℙ¹, for n ≥ 0, dim H^0(𝒪(n)) = n + 1.

theorem RiemannRoch.dimH0_neg (k : Type) [Field k] (n : ℤ) (hn : n < 0) : dimH0 k n = 0

On ℙ¹, for n < 0, dim H^0(𝒪(n)) = 0.

theorem RiemannRoch.dimH1_nonneg (k : Type) [Field k] (m : ℕ) : dimH1 k ↑m = 0

On ℙ¹, for n ≥ 0, dim H^1(𝒪(n)) = 0.

theorem RiemannRoch.dimH1_neg (k : Type) [Field k] (n : ℤ) (hn : n < 0) : dimH1 k n = (-n - 1).toNat

On ℙ¹, for n < 0, dim H^1(𝒪(n)) = -n - 1.

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

Serre duality on ℙ¹: dim H^1(𝒪(n)) = dim H^0(𝒪(-2 - n)).

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

Riemann–Roch on ℙ¹: dim H^0(𝒪(d)) - dim H^1(𝒪(d)) = d + 1.

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

The canonical bundle on ℙ¹ is 𝒪(-2); dim H^0(K) = 0.

theorem RiemannRoch.canonical_bundle_P1_H1 (k : Type) [Field k] : dimH1 k (-2) = 1

The canonical bundle on ℙ¹: dim H^1(K) = 1.

def RiemannRoch.genus (d : ℕ) : ℕ

Genus of a smooth plane curve of degree d: (d - 1)(d - 2) / 2.

theorem RiemannRoch.genus_line : genus 1 = 0

A line in ℙ² has genus 0.

theorem RiemannRoch.genus_conic : genus 2 = 0

A smooth conic in ℙ² has genus 0.

theorem RiemannRoch.genus_cubic : genus 3 = 1

A smooth plane cubic has genus 1 (an elliptic curve).

theorem RiemannRoch.genus_quartic : genus 4 = 3

A smooth plane quartic has genus 3.

theorem RiemannRoch.adjunction_formula_nonneg (d : ℕ) : d * (d - 3) = 2 * genus d - 2

Adjunction formula for a smooth plane curve of degree d: d(d - 3) = 2g - 2.

theorem RiemannRoch.adjunction_formula_alt (d : ℕ) (hd : 3 ≤ d) : d * (d - 3) + 2 = (d - 1) * (d - 2)

Alternative form of the adjunction formula: d(d - 3) + 2 = (d - 1)(d - 2).

noncomputable def RiemannRoch.euler_char (k : Type) [Field k] (n : ℤ) : ℤ

Euler characteristic of 𝒪(n) on ℙ¹: dim H^0 - dim H^1.

theorem RiemannRoch.euler_char_eq (k : Type) [Field k] (n : ℤ) : euler_char k n = n + 1

Euler characteristic formula on ℙ¹: χ(𝒪(n)) = n + 1.

theorem RiemannRoch.euler_char_structure_sheaf (k : Type) [Field k] : euler_char k 0 = 1

Euler characteristic of the structure sheaf on ℙ¹: χ(𝒪) = 1.

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

Serre duality version of Riemann–Roch on ℙ¹: dim H^0(𝒪(d)) - dim H^0(𝒪(-2 - d)) = d + 1.

theorem RiemannRoch.genus_line_eq_dimH1_P1 (k : Type) [Field k] : ↑(genus 1) = ↑(dimH1 k 0)

The genus of a line ℓ ⊆ ℙ² agrees with dim H^1(𝒪_{ℙ¹}) = 0.

theorem RiemannRoch.genus_line_euler_consistency (k : Type) [Field k] : euler_char k 0 = 1 - ↑(genus 1)

Consistency of the Euler characteristic with the genus formula for a line.