Self-duality from a polarization

A polarization of a pure Hodge structure of weight n identifies its complex vector space with its complex dual. The weight of the dual is -n, so the comparison is a Hodge morphism only after twisting the dual by -n; this restores weight n. On the lattice the same map need not be an equivalence: its cokernel records the discriminant of the integral polarizing form. It is always injective, and it is an equivalence exactly when the form is a perfect pairing.

This is the self-duality supplied by the Hodge--Riemann bilinear relations, and it makes duals of polarizable structures polarizable. The inverse form on the dual is in general only rational, since the inverse of an integral form is integral only when the form is a perfect pairing. Instead, the image of the integral self-duality has finite index c, so there is a Hodge morphism V^*(-n) → V inverting self-duality up to the factor c. That morphism is injective, so the polarizing form of V pulls back along it to a polarizing form of V^*(-n), and a Tate twist turns this into a polarizing form of V^*.

Main declarations

• TauCeti.Hodge.HodgeStructure.dualTateTwist: the same-weight target V^*(-n).
• TauCeti.Hodge.Polarization.toDualHom: the Hodge morphism from a polarized structure to the appropriately twisted dual.
• TauCeti.Hodge.Polarization.toDualHom_toLinearMap: its complex action is the polarizing form.
• TauCeti.Hodge.Polarization.toDualHom_toLinearMap_bijective: the complex self-duality is an isomorphism.
• TauCeti.Hodge.Polarization.toDualHom_toIntLinearMap_bijective_iff_isPerfPair: the integral self-duality is an isomorphism exactly for a perfect integral polarizing form.
• TauCeti.Hodge.Polarization.exists_comp_toDualHom_eq_nsmul_id: the integral self-duality is invertible up to a nonzero integer.
• TauCeti.Hodge.IsPolarizable.dual: the dual of a polarizable pure Hodge structure is polarizable.

References

Deligne, Théorie de Hodge II, §2.1; Peters--Steenbrink, Mixed Hodge Structures, §2.1.

noncomputable def TauCeti.Hodge.HodgeStructure.dualTateTwist {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) : HodgeStructure ⋯ n

The Tate twist of the dual that has the same weight as the original Hodge structure.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.dualTateTwist_F {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (p : ℤ) : hs.dualTateTwist.F p = hs.dual.F (p - n)

The filtration of the same-weight dual target is the translated dual filtration.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.dualTateTwist_conjF {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (p : ℤ) : HodgeStructureOn.conjF hs.dualTateTwist p = HodgeStructureOn.conjF hs.dual (p - n)

The conjugate filtration of the same-weight dual target is translated in the same way.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.dualTateTwist_piece {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (p : ℤ) : HodgeStructureOn.piece hs.dualTateTwist p = HodgeStructureOn.piece hs.dual (p - n)

The p-th Hodge component of V^*(-n) is the (p-n)-th component of V^*.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.dualTateTwist_hodgeNumber {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} (hs : HodgeStructure hℂ n) (p : ℤ) : HodgeStructureOn.hodgeNumber hs.dualTateTwist p = HodgeStructureOn.hodgeNumber hs.dual (p - n)

The Hodge numbers of V^*(-n) are the translated Hodge numbers of V^*.

noncomputable def TauCeti.Hodge.Polarization.toDualHom {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : hs.Hom hs.dualTateTwist

A polarization gives an integral Hodge morphism to the (-n)-th Tate twist of the dual.

The twist is forced by weights: the dual has weight -n, and twisting it by -n changes its weight to -n - 2(-n) = n.

@[simp]

theorem TauCeti.Hodge.Polarization.toDualHom_toIntLinearMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : P.toDualHom.toIntLinearMap = P.Qint

The integral linear map underlying self-duality is the integral polarizing form.

@[simp]

theorem TauCeti.Hodge.Polarization.toDualHom_toLinearMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : P.toDualHom.toLinearMap = P.Q

The complex action of polarization self-duality is the complex polarizing form viewed as a linear map to the dual.

theorem TauCeti.Hodge.Polarization.toDualHom_toIntLinearMap_injective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : Function.Injective ⇑P.toDualHom.toIntLinearMap

The integral self-duality map induced by a polarization is injective.

theorem TauCeti.Hodge.Polarization.toDualHom_toLinearMap_injective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : Function.Injective ⇑P.toDualHom.toLinearMap

The complex self-duality map induced by a polarization is injective.

theorem TauCeti.Hodge.Polarization.toDualHom_toLinearMap_bijective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : Function.Bijective ⇑P.toDualHom.toLinearMap

The complex self-duality map induced by a polarization is bijective.

theorem TauCeti.Hodge.Polarization.toDualHom_toIntLinearMap_bijective_iff_isPerfPair {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : Function.Bijective ⇑P.toDualHom.toIntLinearMap ↔ LinearMap.IsPerfPair P.Qint

The integral self-duality map is bijective exactly when the integral polarizing form is a perfect pairing. This is the unimodularity condition on the polarized lattice.

theorem TauCeti.Hodge.Polarization.exists_comp_toDualHom_eq_nsmul_id {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : ∃ (c : ℕ), c ≠ 0 ∧ ∃ (g : hs.dualTateTwist.Hom hs), P.toDualHom.comp g = c • HodgeStructure.Hom.id hs.dualTateTwist ∧ g.comp P.toDualHom = c • HodgeStructure.Hom.id hs

Self-duality is invertible up to a nonzero integer. For a polarization of V, there is a Hodge morphism g : V^*(-n) → V such that composing it with self-duality, in either order, is multiplication by a nonzero natural number c. Over ℚ, c⁻¹ • g is the inverse of self-duality.

theorem TauCeti.Hodge.IsPolarizable.dualTateTwist {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (h : IsPolarizable hℂ hs) : IsPolarizable ⋯ hs.dualTateTwist

The same-weight twist V^*(-n) of the dual of a polarizable pure Hodge structure is polarizable: a polarizing form of V pulls back along an inverse of self-duality up to a nonzero integer.

theorem TauCeti.Hodge.IsPolarizable.dual {V : Type u} {Vℂ : Type v} [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (h : IsPolarizable hℂ hs) : IsPolarizable ⋯ hs.dual

The dual of a polarizable pure Hodge structure is polarizable.