instance GrothendieckBirkhoff.pid_submodule_Rn_free (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (n : ℕ) (N : Submodule R (Fin n → R)) : Module.Free R ↥N

Over a PID, every submodule of R^n is free (used for the Grothendieck-Birkhoff splitting).

noncomputable def GrothendieckBirkhoff.eulerCharP1 (k : Type) [Field k] (n : ℤ) : ℤ

Euler characteristic of O(n) on P^1: χ(O(n)) = dim H^0 - dim H^1.

theorem GrothendieckBirkhoff.eulerCharP1_eq (k : Type) [Field k] (n : ℤ) : eulerCharP1 k n = n + 1

Closed-form Euler characteristic: χ(O_{P^1}(n)) = n + 1.

theorem GrothendieckBirkhoff.eulerCharP1_structure_sheaf (k : Type) [Field k] : eulerCharP1 k 0 = 1

χ(O_{P^1}) = 1.

theorem GrothendieckBirkhoff.genusP1_eq_zero (k : Type) [Field k] : Module.finrank k (SheafCohomology.H1 k 0) = 0

Genus of P^1 is zero: h^1(O_{P^1}) = 0.

def GrothendieckBirkhoff.genus_plane_curve (d : ℕ) : ℕ

Genus of a smooth plane curve of degree d: g = (d - 1)(d - 2)/2, the adjunction formula.

theorem GrothendieckBirkhoff.genus_plane_curve_line : genus_plane_curve 1 = 0

A line (d = 1) has genus zero.

theorem GrothendieckBirkhoff.genus_plane_curve_conic : genus_plane_curve 2 = 0

A smooth conic (d = 2) has genus zero.

theorem GrothendieckBirkhoff.genus_plane_curve_cubic : genus_plane_curve 3 = 1

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

theorem GrothendieckBirkhoff.genus_plane_curve_quartic : genus_plane_curve 4 = 3

A smooth plane quartic (d = 4) has genus 3.

theorem GrothendieckBirkhoff.split_bundle_euler_char (k : Type) [Field k] (n : ℕ) (degrees : Fin n → ℤ) : ∑ i : Fin n, eulerCharP1 k (degrees i) = ∑ i : Fin n, (degrees i + 1)

Euler characteristic of a split bundle on P^1 equals ∑ (d_i + 1).

theorem GrothendieckBirkhoff.split_bundle_rr_P1 (k : Type) [Field k] (n : ℕ) (degrees : Fin n → ℤ) : ∑ i : Fin n, eulerCharP1 k (degrees i) = ∑ i : Fin n, degrees i + ↑n

Riemann-Roch for a split bundle on P^1: χ(⊕ O(d_i)) = (∑ d_i) + n.