Hodge numbers

The p-th Hodge number of a weight-n Hodge structure is the dimension h^{p,n-p} = dim_ℂ H^{p,n-p} of its p-th Hodge component. This file records the two facts that make the family of Hodge numbers a numerical invariant of the structure:

• Hodge symmetry, h^{p,q} = h^{q,p}: the conjugation carries H^{p,n-p} onto H^{n-p,p}. It is only conjugate-linear, so it is not an isomorphism of complex vector spaces; it is an isomorphism of the underlying real vector spaces (TauCeti.Hodge.HodgeStructureOn.pieceConjEquiv, in TauCeti/Geometry/Hodge/Structure.lean), and the two dimensions over ℂ are both half of the common dimension over ℝ.
• The Hodge numbers partition the dimension, ∑ᶠ p, h^{p,n-p} = dim_ℂ V_ℂ: only finitely many Hodge components are nonzero because the filtration is bounded, and they decompose V_ℂ as an internal direct sum.

For a Hodge structure carried on a lattice, dim_ℂ V_ℂ is in turn the rank of the lattice.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.hodgeNumber: the Hodge number h^{p,n-p}.
• TauCeti.Hodge.HodgeStructureOn.finite_setOf_hodgeNumber_ne_zero: only finitely many Hodge numbers are nonzero.
• TauCeti.Hodge.HodgeStructureOn.hodgeNumber_symm: Hodge symmetry.
• TauCeti.Hodge.HodgeStructureOn.finsum_hodgeNumber_eq_finrank: the Hodge numbers sum to the dimension.
• TauCeti.Hodge.finsum_hodgeNumber_eq_finrank_lattice: the Hodge numbers of a Hodge structure carried on a lattice sum to the rank of that lattice.
• TauCeti.Hodge.HodgeStructureOn.isEffective_iff_hodgeNumber_ne_zero: a Hodge structure of weight n is effective exactly when its Hodge numbers are supported in [0, n].
• TauCeti.Hodge.HodgeType: a weight and a symmetric, finitely supported family of Hodge numbers.
• TauCeti.Hodge.HodgeType.IsEffective: a Hodge type whose Hodge numbers are supported in [0, weight].
• TauCeti.Hodge.HodgeStructureOn.hodgeType: the Hodge type of a Hodge structure, effective exactly when the structure is (TauCeti.Hodge.HodgeStructureOn.hodgeType_isEffective_iff).

Voisin, Hodge Theory and Complex Algebraic Geometry I, §6, and Peters–Steenbrink, Mixed Hodge Structures, §2. This is the numerical layer of Layer L3 of TauCetiRoadmap/HodgeStructures/README.md. The signature of HodgeType is adapted from the roadmap's formal companion HodgeStructures/Suggested.lean.

noncomputable def TauCeti.Hodge.HodgeStructureOn.hodgeNumber {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : ℕ

The p-th Hodge number h^{p,n-p} of a weight-n Hodge structure: the complex dimension of its p-th Hodge component.

This follows the convention of Module.finrank, so an infinite-dimensional component has Hodge number 0; the statements that read the Hodge numbers as a dimension count, such as finsum_hodgeNumber_eq_finrank, therefore assume the ambient space is finite-dimensional.

theorem TauCeti.Hodge.HodgeStructureOn.hodgeNumber_def {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.hodgeNumber p = Module.finrank ℂ ↥(hs.piece p)

The Hodge number is the dimension of the Hodge component.

theorem TauCeti.Hodge.HodgeStructureOn.finite_setOf_hodgeNumber_ne_zero {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : {p : ℤ | hs.hodgeNumber p ≠ 0}.Finite

Only finitely many Hodge numbers are nonzero.

theorem TauCeti.Hodge.HodgeStructureOn.hodgeNumber_symm {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.hodgeNumber p = hs.hodgeNumber (n - p)

Hodge symmetry: h^{p,q} = h^{q,p}, where q = n - p.

theorem TauCeti.Hodge.HodgeStructureOn.finsum_hodgeNumber_eq_finrank {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) [FiniteDimensional ℂ W] : ∑ᶠ (p : ℤ), hs.hodgeNumber p = Module.finrank ℂ W

The Hodge numbers partition the dimension: the Hodge numbers of a weight-n Hodge structure on a finite-dimensional complex vector space sum to its dimension.

theorem TauCeti.Hodge.HodgeStructureOn.hodgeNumber_eq_zero_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} [FiniteDimensional ℂ W] (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.hodgeNumber p = 0 ↔ hs.piece p = ⊥

On a finite-dimensional space, a Hodge number vanishes exactly when its Hodge component is zero.

theorem TauCeti.Hodge.HodgeStructureOn.isEffective_iff_hodgeNumber_ne_zero {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} [FiniteDimensional ℂ W] (hs : HodgeStructureOn W ω n) : hs.IsEffective ↔ ∀ (p : ℤ), hs.hodgeNumber p ≠ 0 → p ∈ Set.Icc 0 n

Effectivity in terms of Hodge numbers. A pure Hodge structure of weight n on a finite-dimensional space is effective exactly when its Hodge numbers h^{p,n-p} are supported in 0 ≤ p ≤ n.

structure TauCeti.Hodge.HodgeType : Type

The numerical type of a pure Hodge structure: a weight, Hodge numbers h of finite support, and the Hodge symmetry h p = h (weight - p).

The symmetry is not an extra restriction on the types that occur, since conjugation exchanges the Hodge components H^{p,q} and H^{q,p} of any Hodge structure; it excludes the asymmetric families of numbers that no Hodge structure realizes.

• weight : ℤ

  The weight of the Hodge structures of this type.

• h : ℤ → ℕ

  The prescribed Hodge numbers.

• finite_support : {p : ℤ | self.h p ≠ 0}.Finite

  All but finitely many Hodge numbers vanish.

• symm (p : ℤ) : self.h p = self.h (self.weight - p)

  Hodge symmetry: h^{p,q} = h^{q,p}.

theorem TauCeti.Hodge.HodgeType.ext {x y : HodgeType} (weight : x.weight = y.weight) (h : x.h = y.h) : x = y

theorem TauCeti.Hodge.HodgeType.ext_iff {x y : HodgeType} : x = y ↔ x.weight = y.weight ∧ x.h = y.h

def TauCeti.Hodge.HodgeType.IsEffective (t : HodgeType) : Prop

A Hodge type is effective when its Hodge numbers h p are supported in 0 ≤ p ≤ weight. These are the Hodge types of effective Hodge structures (TauCeti.Hodge.HodgeStructureOn.hodgeType_isEffective_iff).

noncomputable def TauCeti.Hodge.HodgeStructureOn.hodgeType {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : HodgeType

The Hodge type of a Hodge structure: its weight together with its own Hodge numbers.

Both axioms of HodgeType hold for any Hodge structure: the support is finite because the Hodge filtration is bounded, and the symmetry is Hodge symmetry. Following the convention of Module.finrank, an infinite-dimensional Hodge component contributes the Hodge number 0; the statements reading these numbers as a dimension count, such as HodgeStructureOn.finsum_hodgeNumber_eq_finrank, assume finite-dimensionality separately.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.hodgeType_weight {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : hs.hodgeType.weight = n

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.hodgeType_h {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : hs.hodgeType.h = hs.hodgeNumber

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.hodgeType_isEffective_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} [FiniteDimensional ℂ W] (hs : HodgeStructureOn W ω n) : hs.hodgeType.IsEffective ↔ hs.IsEffective

A Hodge structure on a finite-dimensional space is effective exactly when its Hodge type is.

theorem TauCeti.Hodge.finsum_hodgeNumber_eq_finrank_lattice {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Free ℤ V] [Module.Finite ℤ V] {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) : ∑ᶠ (p : ℤ), HodgeStructureOn.hodgeNumber hs p = Module.finrank ℤ V

The Hodge numbers of a Hodge structure on a lattice partition the rank of the lattice.