structure GBGeometric.P1VectorBundle (k : Type u_1) [Field k] : Type

A vector bundle on P^1 of positive rank, presented by its Grothendieck-Birkhoff splitting ⊕ O(d_i) with a decreasing tuple of integer degrees.

• rank : ℕ
• splittingType : Fin self.rank → ℤ
• sorted (i j : Fin self.rank) : i ≤ j → self.splittingType j ≤ self.splittingType i
• hrank_pos : 0 < self.rank

def GBGeometric.P1VectorBundle.degree {k : Type u_1} [Field k] (E : P1VectorBundle k) : ℤ

Total degree of E = ⊕ O(d_i) on P^1: deg E = ∑ d_i.

def GBGeometric.P1VectorBundle.toSplittingType {k : Type u_1} [Field k] (E : P1VectorBundle k) : GBExistence.SplittingType E.rank

Forget the positivity of the rank and recover the abstract SplittingType record.

instance GBGeometric.polynomial_pid (k : Type u_1) [Field k] : IsPrincipalIdealRing (Polynomial k)

k[x] is a principal ideal domain (used to access the structure theorem on P^1).

theorem GBGeometric.pid_structure_theorem (k : Type u_1) [Field k] (M : Type u_2) [AddCommGroup M] [Module (Polynomial k) M] [Module.Finite (Polynomial k) M] [Module.Free (Polynomial k) M] : ∃ (r : ℕ), Nonempty (M ≃ₗ[Polynomial k] Fin r → Polynomial k)

PID structure theorem: a finite free module over k[x] is isomorphic to (k[x])^r for some r.

theorem GBGeometric.pid_rank_unique (k : Type u_1) [Field k] (M : Type u_2) [AddCommGroup M] [Module (Polynomial k) M] [Module.Finite (Polynomial k) M] [Module.Free (Polynomial k) M] (r s : ℕ) (e₁ : M ≃ₗ[Polynomial k] Fin r → Polynomial k) (e₂ : M ≃ₗ[Polynomial k] Fin s → Polynomial k) : r = s

Uniqueness of rank for the PID structure theorem: two trivializations have the same number of summands.

def GBGeometric.splittingTypeToBundle (k : Type u_1) [Field k] {n : ℕ} (hn : 0 < n) (s : GBExistence.SplittingType n) : P1VectorBundle k

Build a P1VectorBundle from an abstract splitting type once a positive-rank witness is given.

theorem GBGeometric.roundtrip_splitting {k : Type u_1} [Field k] (E : P1VectorBundle k) : (splittingTypeToBundle k ⋯ E.toSplittingType).splittingType = E.splittingType

Round-trip through toSplittingType and splittingTypeToBundle recovers the original tuple.

theorem GBGeometric.split_bundle_riemann_roch {k : Type u_1} [Field k] (E : P1VectorBundle k) : ↑(E.toSplittingType.h0_twisted 0) - ↑(E.toSplittingType.h1_twisted 0) = ∑ i : Fin E.rank, E.splittingType i + ↑E.rank

Riemann-Roch for a split bundle on P^1: χ(E) = deg E + rk E.

theorem GBGeometric.split_bundle_euler_from_cech (k : Type) [Field k] (E : P1VectorBundle k) : ∑ i : Fin E.rank, GrothendieckBirkhoff.eulerCharP1 k (E.splittingType i) = E.degree + ↑E.rank

Bridge to Čech computation: the sum of χ(O(d_i)) equals deg E + rk E.

theorem GBGeometric.line_bundle_euler_cech (k : Type) [Field k] (n : ℤ) : ↑(Module.finrank k (SheafCohomology.H0 k n)) - ↑(Module.finrank k (SheafCohomology.H1 k n)) = n + 1

Euler characteristic of O(n) on P^1 via Čech cohomology: χ(O(n)) = n + 1.

theorem GBGeometric.h0_matches_cech (k : Type) [Field k] (d : ℤ) : GBExistence.h0_dim d = Module.finrank k (SheafCohomology.H0 k d)

Combinatorial h^0 matches Čech H^0 dimension for any integer twist d.

theorem GBGeometric.h1_matches_cech (k : Type) [Field k] (d : ℤ) : GBExistence.h1_dim d = Module.finrank k (SheafCohomology.H1 k d)

Combinatorial h^1 matches Čech H^1 dimension for any integer twist d.