Finiteness of coherent cohomology (Theorem 12.18)
DisprovedCondC.finitenessThe first of the four headline theorems of the introduction: on a compact complex manifold, the coherent cohomology groups are finite-dimensional. In the paper this is delivered by Grauert's coherence theorem (Theorem 12.18) - the proper pushforward of a perfect complex along a boundaryless proper map of complex analytic spaces is again perfect - applied to the map to the point. The milestone states the conclusion directly: in the coherent world of a compact complex manifold, every cohomology group of a coherent coefficient carries a finite basis with a spanning coordinate system, the bundled form of finite dimensionality.
Formalization Note The manifold is abstracted by the compact complex world interface; the perfect-complex machinery of Lecture XII that proves the theorem is the proposed work of the milestone.
import Mathlib import Definitions.Def_CondC_liq import Definitions.Def_CondC_geo
namespace CondC
/-! Milestone 5: the finiteness of coherent cohomology. On a compact
complex manifold, every coherent cohomology group is finite-dimensional:
it carries a finite basis with a spanning coordinate system. This is the
first of the four headline theorems of the introduction, delivered by
Grauert's coherence theorem (Theorem 12.18) applied to the map to the
point. -/
theorem finiteness : ∀ (w : CompactCxWorld) (F : Type), w.coherent F → ∀ i : ℕ,
Nonempty (BundledFiniteDim (w.Coh F i) (w.add F i) (w.zero F i) (w.smul F i)) := by sorry
end CondC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in every compact complex world, for every coherent coefficient and every degree, the cohomology group carries the structure of a bundled finite-dimensional space: a finite basis whose spanning map respects the bundled addition, zero, and scalar multiplication, is injective on the coordinate space, and is inverted by the coordinate map. No other hypotheses appear.