19.7. Finiteness.CechFinitenessAssembly🔗

Jacobians.Finiteness.CechFinitenessAssembly — source

finiteDimensional_cechH1_of_chartDiskMontel

Finiteness of H¹(𝔘, 𝒪_D) for an arbitrary finite cover, from the chart-disk Montel finiteness (any divisor D). cechH1 𝔘 D ↪ cechH1 𝔇 D (Forster 12.4 injectivity along a chart-disk refinement 𝔇 ⪯ 𝔘, which is UNCONDITIONAL in D) injects into the finite-dimensional cechH1 𝔇 D; a linear injection into a finite-dimensional space has a finite-dimensional domain. No cover-independence isomorphism is used. The proof is D-agnostic — D enters only through the Montel hypothesis.

theorem finiteDimensional_cechH1_of_chartDiskMontel (D : Divisor X)
    (hMontel : ∀ 𝔇 : ChartDiskCover X, FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 D))
    (𝔘 : FiniteCover X) :
    FiniteDimensional ℂ (𝔘.cechH1 D)

finiteDimensional_cechH1_zero_of_chartDiskMontel

D = 0 specialization of finiteDimensional_cechH1_of_chartDiskMontel.

theorem finiteDimensional_cechH1_zero_of_chartDiskMontel
    (hMontel : ∀ 𝔇 : ChartDiskCover X, FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X)))
    (𝔘 : FiniteCover X) :
    FiniteDimensional ℂ (𝔘.cechH1 (0 : Divisor X))

chartDiskMontel_zero

The chart-disk Montel finiteness, discharged unconditionally (Forster 14.9, D = 0). This is exactly ChartDiskCover.finiteDimensional_cechH1_chartDisk_complete (the leray field / global Bott–Tu (0,1)-form) — packaged as the hMontel hypothesis the assembly above consumes. [Nonempty X] is supplied by [ConnectedSpace X].

theorem chartDiskMontel_zero :
    ∀ 𝔇 : ChartDiskCover X, FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X))

finiteDimensional_cechH1_zero

Finiteness of H¹(𝔘, 𝒪) for an arbitrary finite cover (Forster 14.9, D = 0) — UNCONDITIONAL. Discharges the Montel hypothesis of finiteDimensional_cechH1_zero_of_chartDiskMontel with chartDiskMontel_zero.

theorem finiteDimensional_cechH1_zero (𝔘 : FiniteCover X) :
    FiniteDimensional ℂ (𝔘.cechH1 (0 : Divisor X))