19.9. Finiteness.CechFinitenessWiring🔗

Jacobians.Finiteness.CechFinitenessWiring — source

exists_cechModel

The chart-disk Leray model exists and computes cechH1. Every finite cover 𝔘 and divisor D admits a chart-disk Leray model — a DiskOverlapData (per-overlap chart-images as disks in ℂ, each with a relatively-compact shrinking) and a Coboundaries bundle (the sup-norm δ⁰/δ¹, the restriction commuting square, AND the leray disk-acyclicity witness) — whose sup-norm H¹ is ℂ-linearly isomorphic to the genuine germ-class 𝔘.cechH1 D.

The comparison is bundled into the conclusion (rather than a free-c standalone) precisely because supH1 depends only on the model and cechH1 D only on (𝔘, D): the isomorphism holds only for the model *built from* (𝔘, D).

proven by CechFinitenessDtwist.exists_cechModel_general: the general-divisor finiteness finiteDimensional_cechH1_general (the Forster §16 skyscraper reduction climbing the D = 0 finiteness one point at a time) makes 𝔘.cechH1 D finite-dimensional, and the artificial finite-dimensional Montel model exists_cechModel_of_finiteDimensional then supplies a DiskOverlapData + Coboundaries whose supH1 is ℂ-linearly isomorphic to it. This is exactly the statement of DolbeaultLadder.finiteDimensional_cechH1's model-existence input.

theorem exists_cechModel (𝔘 : FiniteCover X) (D : Divisor X) :
    ∃ (d : DiskOverlapData) (c : Coboundaries d), Nonempty (𝔘.cechH1 D ≃ₗ[ℂ] c.supH1)

finiteDimensional_cechH1_wired

The finiteness node, assembled. H¹(𝔘, 𝒪_D) is finite-dimensional: take the chart-disk Leray model with its comparison (exists_cechModel); its sup-norm H¹ is finite-dimensional by finiteDimensional_supH1 (ρ compact via the Montel atom + the Leray surjectivity leray_surjective); and the bundled comparison cechH1 ≃ₗ supH1 transports finiteness back to the germ-class cechH1. This discharges the exact statement of DolbeaultLadder.finiteDimensional_cechH1.

theorem finiteDimensional_cechH1_wired (𝔘 : FiniteCover X) (D : Divisor X) :
    FiniteDimensional ℂ (𝔘.cechH1 D)