14.4. Cech.CechComplex🔗

Jacobians.Cech.CechComplex — source

FiniteFamily

A finite family of opens of X (no covering condition). The Čech complex and H¹ below are defined at this level, so they apply both to a genuine FiniteCover (covering X) and to a family covering only a chart-disk subregion — the latter is the *inhabited* base for the disk-acyclicity input (H¹(disk, 𝒪) = 0).

structure FiniteFamily (X : Type*) [TopologicalSpace X] where

FiniteCover

A finite open cover of X: a finite family whose sets cover X. For the Leray/Stein property used by finiteness one takes the U i to be chart-disks; that refinement is recorded where needed.

structure FiniteCover (X : Type*) [TopologicalSpace X] extends FiniteFamily X where

IsLeray

A finite family is Leray (for 𝒪): each set is simply connected — a simply-connected open subset of a Riemann surface is biholomorphic to a disk or ℂ, hence H¹(U_i, 𝒪) = 0 (the sets are 𝒪-acyclic).

This is *exactly* the hypothesis under which Čech H¹ computes sheaf cohomology, and no more: every statement needed here is an H¹ statement, and for H¹ Cartan's comparison sequence 0 → Ȟ¹(𝔘, 𝒪) → H¹(X, 𝒪) → Ȟ⁰(𝔘, ℋ¹(𝒪)) is an isomorphism as soon as the cover *sets* are acyclic (then the presheaf ℋ¹(𝒪) : U ↦ H¹(U,𝒪) vanishes on the cover, so Ȟ⁰(𝔘, ℋ¹) = 0). Acyclicity of the *pairwise overlaps* is needed only for H² and higher, so it is not part of this predicate; dropping it makes LerayCoverExists.exists_lerayCover unconditional (chartBallCover_simplyConnected). The chart-disk cover satisfies this.

def IsLeray (𝔘 : FiniteFamily X) : Prop

Cochain0

0-cochains: a germ-class on each ↥(U i).

abbrev Cochain0 : Type _

Cochain1

1-cochains: a germ-class on each pairwise intersection.

abbrev Cochain1 : Type _

Cochain2

2-cochains: a germ-class on each triple intersection.

abbrev Cochain2 : Type _

rawRestrictG_comp_apply

Nested germ restriction collapses to a single one (openIncl composes; the order proofs are irrelevant). The cocycle identity that makes δ² = 0.

theorem rawRestrictG_comp_apply {U V W : Opens X} (h1 : V ≤ U) (h2 : W ≤ V) (f : MGerm U) :
    rawRestrictG h2 (rawRestrictG h1 f) = rawRestrictG (h2.trans h1) f

cechDelta0

Čech differential δ⁰ : C⁰ → C¹, (δ⁰f)_{ij} = f_j|_{U_i∩U_j} − f_i|_{U_i∩U_j}.

noncomputable def cechDelta0 : 𝔘.Cochain0 →ₗ[ℂ] 𝔘.Cochain1

cechDelta1

Čech differential δ¹ : C¹ → C², (δ¹g)_{ijk} = g_{jk}|_{ijk} − g_{ik}|_{ijk} + g_{ij}|_{ijk}.

noncomputable def cechDelta1 : 𝔘.Cochain1 →ₗ[ℂ] 𝔘.Cochain2

cechDelta1_comp_cechDelta0

δ² = 0: the alternating sum of restrictions cancels. Nested restrictions collapse (rawRestrictG_comp), so the six terms g_k − g_j − g_k + g_i + g_j − g_i pair up and vanish.

theorem cechDelta1_comp_cechDelta0 : (𝔘.cechDelta1) ∘ₗ (𝔘.cechDelta0) = 0

sections0

0-cochains that are 𝒪_D-sections on each U i.

def sections0 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    Submodule ℂ 𝔘.Cochain0 where

sections1

1-cochains that are 𝒪_D-sections on each pairwise intersection.

def sections1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    Submodule ℂ 𝔘.Cochain1 where

cocycles1

The 𝒪_D 1-cocycles: ker δ¹ intersected with the 𝒪_D sections.

noncomputable def cocycles1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    Submodule ℂ 𝔘.Cochain1

coboundaries1

The 𝒪_D 1-coboundaries: the image of the 𝒪_D 0-sections under δ⁰.

noncomputable def coboundaries1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    Submodule ℂ 𝔘.Cochain1

cechH1

Čech H¹(𝔘, 𝒪_D) = Z¹/B¹ — cocycles modulo coboundaries, a ℂ-module. The cochains are germ-classes (MGerm, junk-free), so this is the genuine H¹; Z¹/B¹ is the one inherent cohomology quotient. (B¹ ⊆ Z¹ by δ² = 0 + restriction preserving 𝒪_D.)

abbrev cechH1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) : Type _

globalSections

H⁰(𝔘, 𝒪_D) = global matching 𝒪_D-sections = ker δ⁰ ∩ sections. Junk-free (germ-class cochains), so h⁰ below is a plain finrank — no quotient.

noncomputable def globalSections [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    Submodule ℂ 𝔘.Cochain0

h0Dim

h⁰(D) (Forster's h⁰(X, 𝒪_D)) — a plain submodule finrank, junk already quotiented by MGerm.

noncomputable def h0Dim [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) : ℕ

h1Dim

h¹(D) (Forster's h¹(X, 𝒪_D)).

noncomputable def h1Dim [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) : ℕ