theorem GAGA.gaga_pic0_is_complex_torus (g : ℕ) (hg : 0 < g) : ∃ (Λ : AddSubgroup (Fin g → ℂ)), Nonempty (↥Λ ≃+ (Fin (2 * g) → ℤ))

GAGA consequence for Pic⁰(X) of a smooth projective curve of genus g: the connected component of the Picard group is a complex torus ℂᵍ / Λ with Λ a lattice of rank 2g.

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

Algebraic side of GAGA for P¹: the Euler characteristic of O(n) is h⁰ − h¹ = n + 1, matching its analytic counterpart.