Documentation

TauCeti.Geometry.Hodge.TensorProduct.Polarization

Tensor products of polarized Hodge structures #

If Q polarizes an integral pure Hodge structure V of weight n and Q' polarizes V' of weight n', then the tensor product form Q ⊗ Q' polarizes the tensor product V ⊗ V' of weight n + n' (TauCeti.Hodge.HodgeStructure.tensorProduct, carried by the tensor product of the lattices).

The Weil operator of the tensor product is the tensor product of the Weil operators, so the Hodge form of Q ⊗ Q' is the tensor product of the Hodge forms of Q and Q'; as a tensor product of positive definite Hermitian forms it is positive definite, which is the second Hodge–Riemann relation. The first Hodge–Riemann relation holds because the Hodge component H^{p,q} of the tensor product is spanned by the products of the components of V and V' whose bidegrees add up to (p,q). Positivity also gives nondegeneracy, which descends to the integral form because a lattice carrying a nondegenerate form is torsion-free, hence flat over ℤ.

Consequently polarizable Hodge structures are closed under tensor products.

Main declarations #

References #

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

The tensor product of two polarizations #

source
theorem TauCeti.Hodge.IsPolarization.tensorProduct {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} {Q : LinearMap.BilinForm ℤ V} {Q' : LinearMap.BilinForm ℤ V'} (h : IsPolarization hℂ hs Q) (h' : IsPolarization h'ℂ hs' Q') :
IsPolarization ⋯ (hs.tensorProduct hs') (Q.tmul Q')

The tensor product of two polarizing forms polarizes the tensor product. If Q polarizes a Hodge structure of weight n and Q' one of weight n', then Q ⊗ Q' polarizes their tensor product, of weight n + n'.

source
noncomputable def TauCeti.Hodge.Polarization.tensorProduct {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') :
Polarization ⋯ (hs.tensorProduct hs')

The tensor product of two polarizations of pure Hodge structures.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.Polarization.tensorProduct_Qint {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') :
    (P.tensorProduct P').Qint = P.Qint.tmul P'.Qint

    The integral form of a tensor product of polarizations is the tensor product form.

    source
    @[simp]
    theorem TauCeti.Hodge.Polarization.tensorProduct_Q {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') :
    (P.tensorProduct P').Q = P.Q.tmul P'.Q

    The complex form of a tensor product of polarizations is the tensor product form.

    source
    @[simp]
    theorem TauCeti.Hodge.Polarization.tensorProduct_hodgeForm_tmul_tmul {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') (a c : Vℂ) (b d : V'ℂ) :
    ((P.tensorProduct P').hodgeForm (a ⊗ₜ[ℂ] b)) (c ⊗ₜ[ℂ] d) = (P.hodgeForm a) c * (P'.hodgeForm b) d

    The Hodge form of a tensor product of polarizations is the product of their Hodge forms on pure tensors.

    source
    theorem TauCeti.Hodge.IsPolarizable.tensorProduct {V : Type u_1} {V' : Type u_2} {Vℂ : Type u_3} {V'ℂ : Type u_4} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n n' : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n'} (h : IsPolarizable hℂ hs) (h' : IsPolarizable h'ℂ hs') :
    IsPolarizable ⋯ (hs.tensorProduct hs')

    Polarizable Hodge structures are closed under tensor products.