structure CompactKahlerManifold (n : ℕ) : Type (u_1 + 1)

A compact (nonempty) Kähler manifold of complex dimension $n$, abstractly bundled with its topology and the assumption of compactness.

• carrier : Type u_1
• topInst : TopologicalSpace self.carrier
• isCompact : CompactSpace self.carrier
• isNonempty : Nonempty self.carrier

structure BidegreeDecomposition (n : ℕ) (_M : CompactKahlerManifold n) : Type

Hodge / bidegree decomposition data for a compact Kähler manifold: $$b_k = \sum_{p+q=k} h^{p,q}, \qquad h^{p,q} = h^{q,p}, \qquad h^{p,q} = h^{n-q,\,n-p}.$$ The first identity is the Hodge decomposition, the second is complex conjugation symmetry, and the third is Serre / Hodge $\star$ duality.

• hodge : ℕ → ℕ → ℕ
• betti : ℕ → ℕ
• hodge_decomposition (k : ℕ) : self.betti k = ∑ p ∈ Finset.range (k + 1), self.hodge p (k - p)
• conjugation_symmetry (p q : ℕ) : self.hodge p q = self.hodge q p
• star_symmetry (p q : ℕ) : self.hodge p q = self.hodge (n - q) (n - p)

def advanced_kahler_property (n : ℕ) (M : CompactKahlerManifold n) : Prop

The "advanced Kähler property": $M$ carries some bidegree decomposition data. A marker proposition asserting the existence of Hodge data on $M$.

theorem compact_kahler_odd_betti_even_mathlib {n : ℕ} {M : CompactKahlerManifold n} (bd : BidegreeDecomposition n M) (k : ℕ) (hk : k % 2 = 1) : ∃ (m : ℕ), bd.betti k = 2 * m

Odd Betti numbers of a compact Kähler manifold are even. Using the Hodge decomposition $b_k = \sum_{p+q=k} h^{p,q}$ and the conjugation symmetry $h^{p,q} = h^{q,p}$, pairing $(p, k-p)$ with $(k-p, p)$ shows $b_{2j+1}$ is even.