structure SheafCohDerived.CechDeltaFunctorP1 (k : Type) [Field k] : Type

Numerical data for the Čech δ-functor on ℙ¹: the dimensions h⁰(O(n)), h¹(O(n)), their characteristic formulas, and the Euler identity.

• dimH0 : ℤ → ℕ
• dimH1 : ℤ → ℕ
• dimH0_nonneg (n : ℤ) : 0 ≤ n → self.dimH0 n = (n + 1).toNat
• dimH0_neg (n : ℤ) : n < 0 → self.dimH0 n = 0
• dimH1_nonneg (n : ℤ) : 0 ≤ n → self.dimH1 n = 0
• dimH1_neg (n : ℤ) : n < 0 → self.dimH1 n = (-n - 1).toNat
• euler (n : ℤ) : ↑(self.dimH0 n) - ↑(self.dimH1 n) = n + 1

noncomputable def SheafCohDerived.mkCechDeltaFunctorP1 (k : Type) [Field k] : CechDeltaFunctorP1 k

Construct the Čech δ-functor on ℙ¹ from the explicit sheaf cohomology groups H⁰, H¹.

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

Additive step of the Euler characteristic on ℙ¹: χ(O(n+1)) − χ(O(n)) = 1.

theorem SheafCohDerived.serre_duality_derived (k : Type) [Field k] (n : ℤ) : Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

Derived version of Serre duality on ℙ¹: dim H¹(O(n)) = dim H⁰(O(-2 - n)).

theorem SheafCohDerived.cech_effaceability_witness (k : Type) [Field k] (n : ℤ) : ∃ (N : ℤ), 0 ≤ N ∧ n ≤ N ∧ Module.finrank k (SheafCohomology.H1 k N) = 0

Effaceability witness: for every n, there exists N ≥ max 0 n with H¹(O(N)) = 0.