The Tate twist as a tensor product

The Tate twist V(m) of a pure Hodge structure V of weight n is classically defined as the tensor product V ⊗ ℤ(m) with the rank-one Tate structure. The construction TauCeti.Hodge.HodgeStructureOn.tateTwist instead keeps the underlying complex vector space W and shifts the filtration, F^p(V(m)) = F^{p+m}(V). This file compares the two on the complex side: Mathlib's right unitor TensorProduct.rid ℂ W : W ⊗[ℂ] ℂ ≃ₗ[ℂ] W intertwines the conjugations, and the complex Hodge components and the Hodge filtration of V(m) are the pullbacks of those of V ⊗ ℤ(m) along its inverse.

Consequently the weight and filtration shift of tateTwist are those of V ⊗ ℤ(m), the Hodge numbers of V ⊗ ℤ(m) are those of V translated by m, and the Hodge components and filtration of ℤ(k + m) are those of ℤ(k) ⊗ ℤ(m) along the right unitor ℂ ⊗[ℂ] ℂ ≃ₗ[ℂ] ℂ.

The convention follows Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1, and Peters–Steenbrink, Mixed Hodge Structures, §2.1. The comparison of components adapts the decomposition argument of TauCeti.Hodge.HodgeStructureOn.internalHom_piece_eq_comap.

Main declarations

• TauCeti.Hodge.Conjugation.rid_symm_map_conj: the right unitor intertwines a conjugation with its tensor product with the conjugation of the Tate complexification.
• TauCeti.Hodge.HodgeStructureOn.tateTwist_piece_eq_comap and TauCeti.Hodge.HodgeStructureOn.tateTwist_F_eq_comap: the components and the filtration of V(m) are the pullbacks of those of V ⊗ ℤ(m) along the inverse right unitor.
• TauCeti.Hodge.HodgeStructureOn.tensorProduct_tate_hodgeNumber: the Hodge numbers of V ⊗ ℤ(m) are those of V shifted by m.
• TauCeti.Hodge.tate_add_piece_eq_comap and TauCeti.Hodge.tate_add_F_eq_comap: the Hodge components and filtration of ℤ(k + m) are the pullbacks of those of ℤ(k) ⊗ ℤ(m) along the inverse right unitor.

theorem TauCeti.Hodge.Conjugation.rid_symm_map_conj {W : Type u} [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (x : W) : (TensorProduct.rid ℂ W).symm (ω.toEquiv x) = (ω.tensorProduct (latticeConjugation isBaseChange_tateLatticeMap)).toEquiv ((TensorProduct.rid ℂ W).symm x)

The inverse right unitor W ≃ₗ[ℂ] W ⊗[ℂ] ℂ intertwines a conjugation ω of W with the tensor product of ω and the conjugation of the Tate complexification ℂ.

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_piece_eq_comap {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tateTwist m).piece p = Submodule.comap (↑(TensorProduct.rid ℂ W).symm) ((hs.tensorProduct (tate m)).piece p)

The Tate twist is the tensor product with ℤ(m): components. The degree-p component of V(m) is the pullback of the degree-p component of V ⊗ ℤ(m) along the inverse right unitor W ≃ₗ[ℂ] W ⊗[ℂ] ℂ.

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_F_eq_comap {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tateTwist m).F p = Submodule.comap (↑(TensorProduct.rid ℂ W).symm) ((hs.tensorProduct (tate m)).F p)

The Tate twist is the tensor product with ℤ(m): filtration. The filtration step F^p(V(m)) = F^{p+m}(V) is the pullback of the step F^p(V ⊗ ℤ(m)) along the inverse right unitor W ≃ₗ[ℂ] W ⊗[ℂ] ℂ.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tensorProduct_tate_hodgeNumber {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tensorProduct (tate m)).hodgeNumber p = hs.hodgeNumber (p + m)

The Hodge numbers of V ⊗ ℤ(m) are those of V shifted by m.

theorem TauCeti.Hodge.tate_add_piece_eq_comap (k m p : ℤ) : HodgeStructureOn.piece (tate (k + m)) p = Submodule.comap (↑(TensorProduct.rid ℂ ℂ).symm) (HodgeStructureOn.piece ((tate k).tensorProduct (tate m)) p)

The Hodge components of the Tate structure ℤ(k + m) are the pullbacks of those of ℤ(k) ⊗ ℤ(m) along the inverse right unitor ℂ ≃ₗ[ℂ] ℂ ⊗[ℂ] ℂ.

theorem TauCeti.Hodge.tate_add_F_eq_comap (k m p : ℤ) : (tate (k + m)).F p = Submodule.comap (↑(TensorProduct.rid ℂ ℂ).symm) (((tate k).tensorProduct (tate m)).F p)

The Hodge filtration of the Tate structure ℤ(k + m) is the pullback of that of ℤ(k) ⊗ ℤ(m) along the inverse right unitor ℂ ≃ₗ[ℂ] ℂ ⊗[ℂ] ℂ.