The dual of a pure Hodge structure

The dual V^* of a pure Hodge structure of weight n is a pure Hodge structure of weight -n on the complex dual space: its filtration step at index p is the annihilator of the filtration step of index 1 - p of the original structure, and its conjugation is the twisted transpose of the original conjugation, sending a functional φ to v ↦ conj (φ (ω v)). The dual pairing then respects Hodge components of complementary indices: the p-th component of the dual pairs nontrivially only against the component of index -p, and, when W is finite-dimensional, has the same dimension as the (-p)-th component, so dualizing reflects the table of Hodge numbers.

This is one of the companion constructions of Layer L0 of TauCetiRoadmap/HodgeStructures/README.md (the ⊗/Hom/dual companions), following Peters–Steenbrink, Mixed Hodge Structures, §2; it is the base on which the internal hom of Hodge structures is to be built.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.dual: the dual pure Hodge structure, of weight -n; its conjugation is the twisted transpose TauCeti.Hodge.Conjugation.dual, and the opposedness of its filtration holds since dual annihilators carry complements to complements.
• TauCeti.Hodge.HodgeStructureOn.dual_F, …dual_conjF: the step of the dual filtration at index p is the annihilator of the original step 1 - p, and the conjugate step is the annihilator of the original conjugate step 1 - p.
• TauCeti.Hodge.HodgeStructureOn.dual_piece: the components of the dual structure are annihilators of sums of complementary filtration steps.
• TauCeti.Hodge.HodgeStructureOn.finrank_dual_piece: when W is finite-dimensional, the dimension of the p-th component of the dual equals that of the (-p)-th component.
• TauCeti.Hodge.HodgeStructureOn.apply_eq_zero_of_mem_piece_of_ne: the dual pairing vanishes between components unless their indices are complementary.

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

The dual pure Hodge structure, of weight -n.

Its filtration step at index p is the annihilator of the original filtration step of index 1 - p; its conjugation is the twisted transpose TauCeti.Hodge.Conjugation.dual. Opposedness of the dual filtration rests on the fact that dual annihilators carry complements to complements (Subspace.isCompl_dualAnnihilator).

Equations

• hs.dual = { F := fun (p : ℤ) => (hs.F (1 - p)).dualAnnihilator, F_antitone := ⋯, F_top := ⋯, opposed := ⋯ }

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.dual_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.dual.F p = (hs.F (1 - p)).dualAnnihilator

The filtration of the dual Hodge structure is made of dual annihilators of steps.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.dual_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.dual.conjF p = (hs.conjF (1 - p)).dualAnnihilator

The conjugate of a step of the dual filtration is the annihilator of a conjugate step.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.dual_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.dual.piece p = (hs.F (1 - p) ⊔ hs.conjF (n + 1 + p)).dualAnnihilator

A component of the dual Hodge structure is the annihilator of the sum of the two filtration steps flanking the component of complementary index.

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

The dimension of the p-th component of the dual Hodge structure equals the dimension of the (-p)-th component: dualizing reflects the table of Hodge numbers.

theorem TauCeti.Hodge.HodgeStructureOn.apply_eq_zero_of_mem_piece_of_ne {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {a p : ℤ} {u : W} {φ : Module.Dual ℂ W} (hu : u ∈ hs.piece a) (hφ : φ ∈ hs.dual.piece p) (hne : a ≠ -p) : φ u = 0

A functional in the p-th component of the dual vanishes on every component whose index is not -p: the dual pairing pairs the p-th component of the dual only against the component of complementary index.