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. The pairing is invariant under the Weil operators, so the Weil
operator of the dual is the transpose of the inverse Weil operator.
For an integral pure Hodge structure the dual is carried by the dual lattice Hom_ℤ(V, ℤ): the
complex dual of the complexification is a complexification of the dual lattice, whose lattice
conjugation is the twisted transpose (TauCeti.Hodge.latticeConjugation_dual). Dualizing is
contravariantly functorial in morphisms, at both the complex and the integral level.
This is the dual companion to tensor products of pure Hodge structures, following Deligne, Théorie de Hodge II, §2.1, and Peters–Steenbrink, Mixed Hodge Structures, §2.1; the internal Hom of two pure Hodge structures is the tensor product of the dual of the source with the target.
Main declarations #
TauCeti.Hodge.HodgeStructureOn.dual: the dual pure Hodge structure, of weight-n; its conjugation is the twisted transposeTauCeti.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 indexpis the annihilator of the original step1 - p, and the conjugate step is the annihilator of the original conjugate step1 - 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: whenWis finite-dimensional, the dimension of thep-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.TauCeti.Hodge.HodgeStructureOn.weilOperator_dual: the Weil operator of the dual is the transpose of the inverse Weil operator, so that the dual pairing is Weil-invariant (TauCeti.Hodge.HodgeStructureOn.weilOperator_dual_apply_weilOperator).TauCeti.Hodge.HodgeStructureOn.IsMorphism.dualMap: the transpose of a morphism of pure Hodge structures is a morphism between the duals.TauCeti.Hodge.HodgeStructure.dual: the dual of an integral pure Hodge structure, on the dual lattice, withTauCeti.Hodge.HodgeStructure.dual_F,…dual_pieceand…dual_weilOperatoridentifying its filtration, components and Weil operator with those of the complex dual.TauCeti.Hodge.HodgeStructure.Hom.dualMap: the transpose of a morphism of integral pure Hodge structures, withTauCeti.Hodge.HodgeStructure.Hom.dualMap_idand…dualMap_compits contravariant functoriality.
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).
Instances For
The filtration of the dual Hodge structure is made of dual annihilators of steps.
The conjugate of a step of the dual filtration is the annihilator of a conjugate step.
A component of the dual Hodge structure is the annihilator of the sum of the two filtration steps flanking the component of complementary index.
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.
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.
The Weil operator of the dual is the transpose of the inverse Weil operator. On the
p-th component of the dual, of weight -n, it acts by i^{2p+n}, and that is the inverse of
the scalar i^{-2p-n} by which the Weil operator acts on the complementary component of index
-p.
The dual pairing is Weil-invariant: ⟨C φ, C x⟩ = ⟨φ, x⟩.
The transpose of a morphism of pure Hodge structures is a morphism between the duals, in the opposite direction.
The dual of an integral Hodge structure #
The dual of an integral pure Hodge structure of weight n, of weight -n. It is carried by
the dual lattice Hom_ℤ(V, ℤ), and its Hodge filtration is that of the dual of the complex Hodge
structure (HodgeStructure.dual_F).
Instances For
The Hodge filtration of the dual of an integral Hodge structure is that of the dual of the complex Hodge structure.
The Hodge components of the dual of an integral Hodge structure are those of the dual of the complex Hodge structure.
The Weil operator of the dual of an integral Hodge structure is the transpose of the inverse Weil operator.
The transpose of a morphism of integral pure Hodge structures, a morphism between the duals in the opposite direction.
Instances For
The integral map underlying the transpose of a Hodge morphism is the transpose of its integral map.
The transpose of a Hodge morphism acts on a functional by precomposition.
Transposition sends the zero morphism to the zero morphism.
Transposition is additive.
Transposition commutes with negation.
Transposition commutes with subtraction.
Transposition commutes with natural multiples.
Transposition commutes with integer multiples.
The transpose of the identity is the identity.
Transposition reverses composition of Hodge morphisms.