Tensor products of pure Hodge structures

The tensor product of pure Hodge structures is graded by adding bidegrees. We construct its conjugation from the tensor product of the two conjugate-linear involutions and use the internal Hodge decompositions to package the total grading as a pure Hodge structure.

For integral pure Hodge structures, the tensor product is carried by the tensor product of the two lattices: the tensor product of the two complexifications is a complexification of it, whose lattice conjugation is the tensor product of the two lattice conjugations (TauCeti.Hodge.latticeConjugation_tensorProduct).

Main declarations

• TauCeti.Hodge.HodgeStructureOn.tensorProduct: the tensor product pure Hodge structure.
• TauCeti.Hodge.HodgeStructureOn.tensorProduct_piece_eq_iSup: the tensor-product Hodge piece as the supremum of products of Hodge pieces of complementary total degree.
• TauCeti.Hodge.HodgeStructureOn.tensorProduct_F_eq_iSup_piece: the tensor-product filtration as the supremum of products of Hodge pieces.
• TauCeti.Hodge.HodgeStructureOn.tmul_mem_tensorProduct: pure tensors have the expected total Hodge degree.
• TauCeti.Hodge.HodgeStructureOn.weilOperator_tensorProduct: the Weil operator of the tensor product is the tensor product of the Weil operators.
• TauCeti.Hodge.HodgeStructure.tensorProduct: the tensor product of two integral pure Hodge structures, on the tensor product of their lattices.
• TauCeti.Hodge.HodgeStructure.tensorProduct_weilOperator: the Weil operator of the integral tensor product is the tensor product of the two Weil operators.

noncomputable def TauCeti.Hodge.HodgeStructureOn.tensorProduct {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ω₁ : Conjugation W₁} {ω₂ : Conjugation W₂} {n₁ n₂ : ℤ} (hs₁ : HodgeStructureOn W₁ ω₁ n₁) (hs₂ : HodgeStructureOn W₂ ω₂ n₂) : HodgeStructureOn (TensorProduct ℂ W₁ W₂) (ω₁.tensorProduct ω₂) (n₁ + n₂)

The tensor product pure Hodge structure, whose weight is the sum of the weights.

theorem TauCeti.Hodge.HodgeStructureOn.tensorProduct_F_eq_iSup_piece {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ω₁ : Conjugation W₁} {ω₂ : Conjugation W₂} {n₁ n₂ : ℤ} (hs₁ : HodgeStructureOn W₁ ω₁ n₁) (hs₂ : HodgeStructureOn W₂ ω₂ n₂) (p : ℤ) : (hs₁.tensorProduct hs₂).F p = ⨆ (q : ℤ), ⨆ (_ : p ≤ q), ⨆ (r : ℤ), Submodule.map₂ (TensorProduct.mk ℂ W₁ W₂) (hs₁.piece r) (hs₂.piece (q - r))

The tensor-product filtration is the supremum of products of Hodge pieces of total degree at least p.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tensorProduct_piece_eq_iSup {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ω₁ : Conjugation W₁} {ω₂ : Conjugation W₂} {n₁ n₂ : ℤ} (hs₁ : HodgeStructureOn W₁ ω₁ n₁) (hs₂ : HodgeStructureOn W₂ ω₂ n₂) (p : ℤ) : (hs₁.tensorProduct hs₂).piece p = ⨆ (r : ℤ), Submodule.map₂ (TensorProduct.mk ℂ W₁ W₂) (hs₁.piece r) (hs₂.piece (p - r))

The tensor-product Hodge piece is the supremum of products of pieces of complementary total degree.

theorem TauCeti.Hodge.HodgeStructureOn.tmul_mem_tensorProduct {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ω₁ : Conjugation W₁} {ω₂ : Conjugation W₂} {n₁ n₂ : ℤ} (hs₁ : HodgeStructureOn W₁ ω₁ n₁) (hs₂ : HodgeStructureOn W₂ ω₂ n₂) {p q : ℤ} {x : W₁} {y : W₂} (hx : x ∈ hs₁.piece p) (hy : y ∈ hs₂.piece q) : x ⊗ₜ[ℂ] y ∈ (hs₁.tensorProduct hs₂).piece (p + q)

A pure tensor of vectors in Hodge degrees p and q has degree p + q.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.weilOperator_tensorProduct {W₁ : Type u} {W₂ : Type v} [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ω₁ : Conjugation W₁} {ω₂ : Conjugation W₂} {n₁ n₂ : ℤ} (hs₁ : HodgeStructureOn W₁ ω₁ n₁) (hs₂ : HodgeStructureOn W₂ ω₂ n₂) : (hs₁.tensorProduct hs₂).weilOperator = TensorProduct.map hs₁.weilOperator hs₂.weilOperator

The Weil operator of a tensor product of pure Hodge structures is the tensor product of the two Weil operators: on a product of components of degrees r and p - r both act by i^(2r-n₁) i^(2(p-r)-n₂) = i^(2p-(n₁+n₂)).

The tensor product of two integral Hodge structures

noncomputable def TauCeti.Hodge.HodgeStructure.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') : HodgeStructure ⋯ (n + n')

The tensor product of two integral pure Hodge structures, of weight the sum of the weights. It is carried by the tensor product of the lattices, and its Hodge filtration is that of the tensor product of the complex Hodge structures (HodgeStructure.tensorProduct_F).

@[simp]

theorem TauCeti.Hodge.HodgeStructure.tensorProduct_F {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 : ℤ) : (hs.tensorProduct hs').F p = (HodgeStructureOn.tensorProduct hs hs').F p

The Hodge filtration of the tensor product of two integral Hodge structures is that of the tensor product of the complex Hodge structures.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.tensorProduct_piece {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 : ℤ) : HodgeStructureOn.piece (hs.tensorProduct hs') p = (HodgeStructureOn.tensorProduct hs hs').piece p

The Hodge components of the tensor product of two integral Hodge structures are those of the tensor product of the complex Hodge structures.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.tensorProduct_weilOperator {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') : HodgeStructureOn.weilOperator (hs.tensorProduct hs') = TensorProduct.map (HodgeStructureOn.weilOperator hs) (HodgeStructureOn.weilOperator hs')

The Weil operator of the integral tensor product is the tensor product of the Weil operators.