24.4. SerrePairing.DolbeaultLadder🔗

Jacobians.SerrePairing.DolbeaultLadder — source

finiteDimensional_cechH1

Finiteness (Forster Thm 14.9). H¹(𝔘, 𝒪_D) is finite-dimensional. Engine: the cochain restriction between a cover and a relatively-compact shrinking is *compact* (disk-Montel: Mathlib Analysis.Complex.LocallyUniformLimit + Arzelà–Ascoli), and a compact perturbation has finite-codimensional image (Schwartz / Riesz–Schauder, via Mathlib IsCompactOperator + RieszLemma).

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