Polarizability of internal homs

The integral internal hom of two polarizable pure Hodge structures is polarizable. Its lattice Hom_ℤ(V, W) is identified with V* ⊗ W by Mathlib's dualTensorHomEquiv; the complexification of this identification respects the Hodge filtrations, by TauCeti.Hodge.HodgeStructureOn.internalHom_F_eq_comap.

A polarizing form on the dual of V and a polarizing form on W therefore give a polarizing form on the internal hom: pull their tensor product back along the inverse contraction. The dual polarization exists without unimodularity of the original integral form, by TauCeti.Hodge.IsPolarizable.dual.

Main results

• TauCeti.Hodge.IsPolarization.internalHom: the pullback of the tensor product of polarizing forms on V* and W polarizes their internal hom.
• TauCeti.Hodge.IsPolarizable.internalHom: polarizable pure Hodge structures are closed under internal homs.

References

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

theorem TauCeti.Hodge.IsPolarization.internalHom {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [Module.Free ℤ V₁] [Module.Finite ℤ V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂} {n₁ n₂ : ℤ} {hs₁ : HodgeStructure h₁ n₁} {hs₂ : HodgeStructure h₂ n₂} {Q₁ : LinearMap.BilinForm ℤ (Module.Dual ℤ V₁)} {Q₂ : LinearMap.BilinForm ℤ V₂} (hQ₁ : IsPolarization ⋯ hs₁.dual Q₁) (hQ₂ : IsPolarization h₂ hs₂ Q₂) : IsPolarization ⋯ (hs₁.internalHom hs₂) (LinearMap.BilinForm.comp (Q₁.tmul Q₂) (↑(dualTensorHomEquiv ℤ V₁ V₂).symm).toAddMonoidHom.toIntLinearMap (↑(dualTensorHomEquiv ℤ V₁ V₂).symm).toAddMonoidHom.toIntLinearMap)

Polarizing forms on the dual of the source and on the target induce a polarization of the integral internal hom, by pulling their tensor product back along the inverse contraction.

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

Polarizable pure Hodge structures are closed under internal homs. The internal hom of weights n₁ and n₂ is polarizable of weight n₂ - n₁.