class HasKahlerHodgeNumbers {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] extends HasHodgeNumbers : Type

A Kähler manifold with Hodge number data, additionally tracking the integral $\int_M \omega^n$ of the top power of the Kähler form.

• complexDim : ℕ
• hodge : ℕ → ℕ → ℕ
• conjugation_symmetry (p q : ℕ) : hodge Ω VF p q = hodge Ω VF q p
• star_symmetry (p q : ℕ) : hodge Ω VF p q = hodge Ω VF (complexDim Ω VF - q) (complexDim Ω VF - p)
• betti : ℕ → ℕ
• betti_hodge_link (k : ℕ) : betti Ω VF k = ∑ p ∈ Finset.range (k + 1), hodge Ω VF p (k - p)
• omega_n_integral : ℝ

theorem HasKahlerHodgeNumbers.omega_n_integral_pos_ax {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hH : HasKahlerHodgeNumbers) : 0 < omega_n_integral Ω VF

Axiom: $\int_M \omega^n > 0$ on a Kähler manifold (since $\omega^n$ is a volume form).

theorem HasKahlerHodgeNumbers.stokes_exact_vanishes_ax {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hH : HasKahlerHodgeNumbers) : HasHodgeNumbers.hodge Ω VF (HasHodgeNumbers.complexDim Ω VF) (HasHodgeNumbers.complexDim Ω VF) = 0 → omega_n_integral Ω VF = 0

Axiom: if $h^{n,n} = 0$ then $\omega^n$ is exact and Stokes implies $\int_M \omega^n = 0$.

theorem HasKahlerHodgeNumbers.omega_factor_vanishes_ax {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (hH : HasKahlerHodgeNumbers) (p : ℕ) : p ≤ HasHodgeNumbers.complexDim Ω VF → HasHodgeNumbers.hodge Ω VF p p = 0 → omega_n_integral Ω VF = 0

Axiom: if $h^{p,p} = 0$ for some $p \leq n$, then $\omega^p$ is exact and the integral $\int_M \omega^n = 0$ (via the Hard Lefschetz factorization $\omega^n = L^{n-p} \omega^p$).

theorem HasKahlerHodgeNumbers.omega_n_integral_pos_thm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hH : HasKahlerHodgeNumbers] : 0 < omega_n_integral Ω VF

Instance-form version: $\int_M \omega^n > 0$.

theorem HasKahlerHodgeNumbers.stokes_exact_vanishes_thm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hH : HasKahlerHodgeNumbers] : HasHodgeNumbers.hodge Ω VF (HasHodgeNumbers.complexDim Ω VF) (HasHodgeNumbers.complexDim Ω VF) = 0 → omega_n_integral Ω VF = 0

Instance-form version of the Stokes vanishing implication for $h^{n,n} = 0$.

theorem HasKahlerHodgeNumbers.omega_factor_vanishes_thm {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hH : HasKahlerHodgeNumbers] (p : ℕ) : p ≤ HasHodgeNumbers.complexDim Ω VF → HasHodgeNumbers.hodge Ω VF p p = 0 → omega_n_integral Ω VF = 0

Instance-form version: $h^{p,p} = 0$ for any $p \leq n$ forces $\int_M \omega^n = 0$.

theorem HasKahlerHodgeNumbers.volume_class_nonzero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hH : HasKahlerHodgeNumbers] : 1 ≤ HasHodgeNumbers.hodge Ω VF (HasHodgeNumbers.complexDim Ω VF) (HasHodgeNumbers.complexDim Ω VF)

On a compact Kähler manifold, the volume class is nonzero: $h^{n,n} \geq 1$.

theorem HasKahlerHodgeNumbers.omega_power_factoring {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hH : HasKahlerHodgeNumbers] (p : ℕ) (hp : p ≤ HasHodgeNumbers.complexDim Ω VF) : 1 ≤ HasHodgeNumbers.hodge Ω VF p p

Each Hodge number $h^{p,p}$ for $p \leq n$ is at least 1 on a compact Kähler manifold, since $[\omega^p] \neq 0$ in $H^{p,p}$.

class HasHardLefschetzPairing {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] extends HasCohomologyWithLefschetz : Type (u_3 + 1)

A cohomology theory equipped with the Hard Lefschetz pairing $Q(n,k)$ on $H^k$, biadditive in both arguments and ℝ-linear in the left.

• H : ℕ → Type u_3
• H_addCommGroup (k : ℕ) : AddCommGroup (H Ω VF k)
• H_module (k : ℕ) : Module ℝ (H Ω VF k)
• H_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H Ω VF k)
• L_map (k m : ℕ) : HasCohomology.H Ω VF k →ₗ[ℝ] HasCohomology.H Ω VF (k + 2 * m)
• Q (_n k : ℕ) : HasCohomology.H Ω VF k → HasCohomology.H Ω VF k → ℝ
• Q_add_left (n k : ℕ) (α₁ α₂ β : HasCohomology.H Ω VF k) : Q n k (α₁ + α₂) β = Q n k α₁ β + Q n k α₂ β
• Q_add_right (n k : ℕ) (α β₁ β₂ : HasCohomology.H Ω VF k) : Q n k α (β₁ + β₂) = Q n k α β₁ + Q n k α β₂
• Q_smul_left (n k : ℕ) (r : ℝ) (α β : HasCohomology.H Ω VF k) : Q n k (r • α) β = r * Q n k α β

class HasLefschetzDecomposition {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] extends HasCohomologyWithLefschetz : Type (u_3 + 1)

The Lefschetz decomposition of cohomology: every class $\alpha \in H^k$ decomposes as $\alpha = \sum_r L^r \alpha_{k-2r}^{\text{prim}}$, where the primitive components are characterized by $L^{n-(k-2r)+1} \alpha_{k-2r}^{\text{prim}} = 0$.

• H : ℕ → Type u_3
• H_addCommGroup (k : ℕ) : AddCommGroup (H Ω VF k)
• H_module (k : ℕ) : Module ℝ (H Ω VF k)
• H_finiteDimensional (k : ℕ) : FiniteDimensional ℝ (H Ω VF k)
• L_map (k m : ℕ) : HasCohomology.H Ω VF k →ₗ[ℝ] HasCohomology.H Ω VF (k + 2 * m)
• prim_component (_n k r : ℕ) : HasCohomology.H Ω VF k →ₗ[ℝ] HasCohomology.H Ω VF (k - 2 * r)
• prim_component_is_primitive (n k r : ℕ) (_hkn : k ≤ n) (_hr : 2 * r ≤ k) (α : HasCohomology.H Ω VF k) : (HasCohomologyWithLefschetz.L_map (k - 2 * r) (n - (k - 2 * r) + 1)) ((prim_component n k r) α) = OfNat.ofNat 0
• reconstruct (_n k : ℕ) : HasCohomology.H Ω VF k → HasCohomology.H Ω VF k
• reconstruct_eq (n k : ℕ) (_hkn : k ≤ n) (α : HasCohomology.H Ω VF k) : reconstruct n k α = α
• prim_component_injective (n k : ℕ) (_hkn : k ≤ n) (α : HasCohomology.H Ω VF k) : (∀ (r : ℕ), 2 * r ≤ k → (prim_component n k r) α = OfNat.ofNat 0) → α = OfNat.ofNat 0