structure SheafCohCurvesFiniteness.CechComplex2 (k : Type u_2) [Field k] : Type (max (max u_2 (u_3 + 1)) (u_4 + 1))

A two-term Čech complex C⁰ → C¹ over a field k: the natural model for the Čech cohomology of a sheaf on a two-element open cover.

• C0 : Type u_3
• C1 : Type u_4
• inst0 : AddCommGroup self.C0
• inst1 : AddCommGroup self.C1
• mod0 : Module k self.C0
• mod1 : Module k self.C1
• d : self.C0 →ₗ[k] self.C1

def SheafCohCurvesFiniteness.CechComplex2.H0 (k : Type u_1) [Field k] (C : CechComplex2 k) : Submodule k C.C0

H⁰ of a two-term Čech complex is the kernel of d : C⁰ → C¹.

@[reducible, inline]

abbrev SheafCohCurvesFiniteness.CechComplex2.H1 (k : Type u_1) [Field k] (C : CechComplex2 k) : Type u_2

H¹ of a two-term Čech complex is the cokernel C¹ / im d.

theorem SheafCohCurvesFiniteness.cech2_higher_vanishing_finrank (k : Type u_1) [Field k] : Module.finrank k (PUnit.{u_2 + 1} ⧸ ⊤) = 0

Vanishing of higher Čech cohomology: the quotient of PUnit by ⊤ has finrank zero (trivially), illustrating H^i = 0 for i ≥ 2 in a two-term complex.

@[reducible]

noncomputable def SheafCohCurvesFiniteness.finiteDim_supported (k : Type) [Field k] (S : Set ℤ) [Fintype ↑S] : Module.Finite k ↥(Finsupp.supported k k S)

The subspace of Finsupp supported in a finite set S is finite-dimensional.

instance SheafCohCurvesFiniteness.cechH0_finiteDim_P1 (k : Type) [Field k] (n : ℤ) : Module.Finite k ↥(CohomologyP1.CechH0 k n)

Finiteness of H⁰(O_{ℙ¹}(n)): it is k-supported on the finite set [0, n].

instance SheafCohCurvesFiniteness.cechH1_finiteDim_P1 (k : Type) [Field k] (n : ℤ) : Module.Finite k ((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n)

Finiteness of H¹(O_{ℙ¹}(n)): it is realized by Laurent terms with indices strictly between n and 0, a finite range.