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.

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.

The construction supplies the tensor-product companion requested in Layer 0 of the HodgeStructures roadmap.

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.

Equations

• hs₁.tensorProduct hs₂ = TauCeti.Hodge.HodgeStructureOn.ofDecomposition ⋯

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.