def GBExistence.h0_dim (d : ℤ) : ℕ

Combinatorial model for h⁰(P¹, O(d)) = max(d + 1, 0).

def GBExistence.h1_dim (d : ℤ) : ℕ

Combinatorial model for h¹(P¹, O(d)) = max(−d − 1, 0) (Serre duality).

theorem GBExistence.h1_dim_of_nonneg {d : ℤ} (hd : 0 ≤ d) : h1_dim d = 0

h¹ vanishes for non-negative twists.

theorem GBExistence.h0_dim_neg {d : ℤ} (hd : d < -1) : h0_dim d = 0

h⁰ vanishes for twists below −1.

theorem GBExistence.h0_dim_nonpos {d : ℤ} (hd : d ≤ -1) : h0_dim d = 0

h⁰ vanishes for twists ≤ −1.

theorem GBExistence.h0_dim_pos {d : ℤ} (hd : 0 ≤ d) : 0 < h0_dim d

For non-negative twists, h⁰(O(d)) > 0.

theorem GBExistence.euler_char_formula (d : ℤ) : ↑(h0_dim d) - ↑(h1_dim d) = d + 1

Combinatorial Riemann-Roch on P¹: h⁰(O(d)) − h¹(O(d)) = d + 1.

theorem GBExistence.h1_vanishes_ge_neg1 {d : ℤ} (hd : -1 ≤ d) : h1_dim d = 0

h¹(O(d)) = 0 for d ≥ −1.

def GBExistence.h0_total {n : ℕ} (degrees : Fin n → ℤ) : ℕ

Total h⁰ of a direct sum ⊕ O(d_i) indexed by Fin n.

def GBExistence.h1_total {n : ℕ} (degrees : Fin n → ℤ) : ℕ

Total h¹ of a direct sum ⊕ O(d_i) indexed by Fin n.

def GBExistence.ext1_dim (a b : ℤ) : ℕ

Dimension of Ext¹(O(a), O(b)) = H¹(O(b − a)) on P¹.

theorem GBExistence.ext1_dim_zero_of_le {a b : ℤ} (h : a ≤ b) : ext1_dim a b = 0

Ext¹(O(a), O(b)) = 0 when a ≤ b, i.e. the splitting obstruction vanishes for line bundles in non-increasing order.

theorem GBExistence.pid_torsionFree_free (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.IsTorsionFree R M] : Module.Free R M

Finitely generated torsion-free modules over a PID are free: this is the key algebraic input for splitting on P¹.

structure GBExistence.SplittingType (n : ℕ) : Type

A splitting type: the data of n integer degrees (d_1 ≥ … ≥ d_n) specifying a candidate decomposition ⊕ O(d_i) in Grothendieck-Birkhoff.

• degrees : Fin n → ℤ
• sorted (i j : Fin n) : i ≤ j → self.degrees j ≤ self.degrees i

def GBExistence.SplittingType.h0_twisted {n : ℕ} (s : SplittingType n) (t : ℤ) : ℕ

h⁰(⊕ O(d_i + t)) for a splitting type s twisted by t.

def GBExistence.SplittingType.h1_twisted {n : ℕ} (s : SplittingType n) (t : ℤ) : ℕ

h¹(⊕ O(d_i + t)) for a splitting type s twisted by t.

def GBExistence.SplittingType.maxDegree {n : ℕ} (s : SplittingType (n + 1)) : ℤ

The maximum degree d_1 in a non-empty splitting type.

theorem GBExistence.SplittingType.le_maxDegree {n : ℕ} (s : SplittingType (n + 1)) (i : Fin (n + 1)) : s.degrees i ≤ s.maxDegree

Every degree in a splitting type is bounded above by the maximum degree.

def GBExistence.SplittingType.tail {n : ℕ} (s : SplittingType (n + 1)) : SplittingType n

The splitting type obtained by removing the first (maximal) summand.

theorem GBExistence.h0_split_decomp {n : ℕ} (s : SplittingType (n + 1)) (t : ℤ) : s.h0_twisted t = h0_dim (s.maxDegree + t) + s.tail.h0_twisted t

Decomposition of h⁰_twisted along the leading summand: h⁰(O(d_1 + t)) + h⁰(⊕_{i≥2} O(d_i + t)).

theorem GBExistence.h1_split_decomp {n : ℕ} (s : SplittingType (n + 1)) (t : ℤ) : s.h1_twisted t = h1_dim (s.maxDegree + t) + s.tail.h1_twisted t

Analogous decomposition for h¹_twisted.

theorem GBExistence.inductive_ext1_vanishing {n : ℕ} (s : SplittingType (n + 1)) : ∑ i : Fin n, ext1_dim (s.tail.degrees i) s.maxDegree = 0

Inductive Ext¹ vanishing: extensions of the tail summands by O(maxDegree) all vanish, since each tail degree is ≤ the maximum degree.

theorem GBExistence.degrees_le_zero_of_h0_twist_vanish {n : ℕ} (degrees : Fin n → ℤ) (h : (h0_total fun (i : Fin n) => degrees i - 1) = 0) (i : Fin n) : degrees i ≤ 0

Reverse engineering: if the total h⁰ of ⊕ O(d_i − 1) vanishes, then every d_i ≤ 0.

theorem GBExistence.split_riemann_roch {n : ℕ} (s : SplittingType n) (t : ℤ) : ↑(s.h0_twisted t) - ↑(s.h1_twisted t) = ∑ i : Fin n, (s.degrees i + t + 1)

Riemann-Roch for a splitting type: the Euler characteristic of ⊕ O(d_i + t) equals Σ (d_i + t + 1).

theorem GBExistence.split_total_degree {n : ℕ} (s : SplittingType n) : ↑(s.h0_twisted 0) - ↑(s.h1_twisted 0) = ∑ i : Fin n, s.degrees i + ↑n

Specialization at t = 0: χ(⊕ O(d_i)) = (Σ d_i) + n.

theorem GBExistence.split_euler_additive {n : ℕ} (s : SplittingType (n + 1)) (t : ℤ) : ↑(s.h0_twisted t) - ↑(s.h1_twisted t) = ↑(h0_dim (s.maxDegree + t)) - ↑(h1_dim (s.maxDegree + t)) + (↑(s.tail.h0_twisted t) - ↑(s.tail.h1_twisted t))

Additivity of Euler characteristic along the splitting: the leading summand and the tail contribute independently.

theorem GBExistence.normalized_has_section {n : ℕ} (s : SplittingType (n + 1)) (h_max : s.maxDegree = 0) : 0 < s.h0_twisted 0

A normalized splitting type with maxDegree = 0 has positive h⁰, since its leading summand is O.

theorem GBExistence.h0_dim_matches_cohomology (k : Type) [Field k] (d : ℤ) (hd : 0 ≤ d) : h0_dim d = Module.finrank k (SheafCohomology.H0 k d)

Bridge: the combinatorial h0_dim matches the actual cohomology dimension of H⁰(P¹, O(d)) for d ≥ 0.

theorem GBExistence.h0_dim_matches_cohomology_neg (k : Type) [Field k] (d : ℤ) (hd : d < 0) : h0_dim d = Module.finrank k (SheafCohomology.H0 k d)

Bridge: the combinatorial h0_dim matches dim H⁰(P¹, O(d)) for d < 0, where both vanish.

theorem GBExistence.h1_dim_matches_cohomology (k : Type) [Field k] (d : ℤ) (hd : 0 ≤ d) : h1_dim d = Module.finrank k (SheafCohomology.H1 k d)

Bridge: the combinatorial h1_dim matches dim H¹(P¹, O(d)) for d ≥ 0, where both vanish.

theorem GBExistence.h1_dim_matches_cohomology_neg (k : Type) [Field k] (d : ℤ) (hd : d < 0) : h1_dim d = Module.finrank k (SheafCohomology.H1 k d)

Bridge: the combinatorial h1_dim matches dim H¹(P¹, O(d)) for d < 0.