def DerivedFunctorsDefs.CohomDeltaFunctor.idMorphism {C : Type u₀} [CategoryTheory.Category.{v₀, u₀} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CohomDeltaFunctor C D) : F.Morphism F

The identity morphism on a cohomological delta functor.

@[simp]

theorem DerivedFunctorsDefs.CohomDeltaFunctor.idMorphism_η {C : Type u₀} [CategoryTheory.Category.{v₀, u₀} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CohomDeltaFunctor C D) (n : ℕ) : F.idMorphism.η n = CategoryTheory.CategoryStruct.id (F.T n)

The n-th component of the identity morphism on a cohomological delta functor is the identity.

theorem CohomologyConnection.rightDerived_effaceable_at {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] [CategoryTheory.Abelian C'] [CategoryTheory.EnoughInjectives C'] {D' : Type u_1} [CategoryTheory.Category.{u_2, u_1} D'] [CategoryTheory.Abelian D'] (F : CategoryTheory.Functor C' D') [F.Additive] (n : ℕ) (X : C') : ∃ (I : C') (i : X ⟶ I), CategoryTheory.Mono i ∧ CategoryTheory.Limits.IsZero ((F.rightDerived (n + 1)).obj I)

For any additive functor on a category with enough injectives, the right derived functors of positive degree are effaceable: each object embeds into an injective whose higher derived images vanish.

structure CohomologyConnection.CechToDerivedDataP1Witness (k : Type) [Field k] : Prop

Witness data packaging the basic facts about Čech-versus-derived cohomology of line bundles on P¹: vanishing of H¹ for nonnegative twists, the Euler characteristic formula, an effaceability witness, and Serre duality.

• h1_vanishing (n : ℤ) : 0 ≤ n → Module.finrank k (SheafCohomology.H1 k n) = 0
• euler_char (n : ℤ) : ↑(Module.finrank k (SheafCohomology.H0 k n)) - ↑(Module.finrank k (SheafCohomology.H1 k n)) = n + 1
• effaceability (n : ℤ) : ∃ (N : ℤ), 0 ≤ N ∧ n ≤ N ∧ Module.finrank k (SheafCohomology.H1 k N) = 0
• serre_duality (n : ℤ) : Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

def CohomologyConnection.mkCechToDerivedDataP1Witness (k : Type) [Field k] : CechToDerivedDataP1Witness k

Concrete construction of the CechToDerivedDataP1Witness for P¹ over k, drawing on the SheafCohomology and SheafCohDerived lemmas.

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

The effaceability witness extracted from the assembled P¹ Čech-to-derived data.

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

The Euler characteristic identity h⁰(O(n)) - h¹(O(n)) = n + 1 on P¹, packaged through the witness.