Tate twists of pure Hodge structures

The m-th Tate twist of a pure Hodge structure of weight n has weight n - 2m and filtration F^p(V(m)) = F^{p+m}(V). The underlying lattice and complex vector space are unchanged: this presents V ⊗ ℤ(m) through the canonical identifications V ⊗_ℤ ℤ ≃ V and V_ℂ ⊗_ℂ ℂ ≃ V_ℂ. Thus the construction works directly with the abstract base-change interface and introduces no choice of tensor-product equivalence. Its complex Hodge components and filtration are those of the tensor product TauCeti.Hodge.HodgeStructureOn.tensorProduct with ℤ(m) along Mathlib's right unitor: see TauCeti.Hodge.HodgeStructureOn.tateTwist_piece_eq_comap and TauCeti.Hodge.HodgeStructureOn.tateTwist_F_eq_comap in TauCeti.Geometry.Hodge.Tate.TensorProduct.

The shift carries Hodge components and Hodge numbers by the same translation. It also acts on morphisms. A polarizing form for V polarizes V(m) unchanged: subtracting the even integer 2m does not change the symmetry sign, while both the filtration indices and the exponent in the Hodge–Riemann positivity relation shift compatibly.

This is the Tate-twist companion in Layer L0 of TauCetiRoadmap/HodgeStructures/README.md. The convention follows Voisin, Hodge Theory and Complex Algebraic Geometry I, §§7.1–7.2.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.tateTwist: the Tate twist of a pure Hodge structure.
• TauCeti.Hodge.HodgeStructureOn.tateTwist_piece: its component in degree p is the original component in degree p + m.
• TauCeti.Hodge.HodgeStructure.Hom.tateTwist: the induced operation on Hodge morphisms.
• TauCeti.Hodge.IsPolarization.tateTwist: a polarizing form remains polarizing after twisting.
• TauCeti.Hodge.IsPolarization.of_F_eq_F_add: the same for a structure that is a Tate twist only up to the identification of propositionally equal weights.
• TauCeti.Hodge.Polarization.tateTwist: the corresponding bundled polarization.

def TauCeti.Hodge.HodgeStructureOn.tateTwist {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m : ℤ) : HodgeStructureOn W ω (n - 2 * m)

The m-th Tate twist of a pure Hodge structure of weight n.

Its weight is n - 2m, and its filtration is shifted by m. The unchanged underlying vector space is the canonical presentation of tensoring with the one-dimensional Tate structure.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_zero {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {h : HodgeStructureOn W ω (n - 2 * 0) = HodgeStructureOn W ω n} : cast h (hs.tateTwist 0) = hs

Twisting by zero leaves a Hodge structure unchanged.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_add {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m k : ℤ) {h : HodgeStructureOn W ω (n - 2 * m - 2 * k) = HodgeStructureOn W ω (n - 2 * (m + k))} : cast h ((hs.tateTwist m).tateTwist k) = hs.tateTwist (m + k)

Two successive Tate twists combine by adding their indices.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tateTwist m).F p = hs.F (p + m)

The Hodge filtration of a Tate twist is the translated original filtration.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tateTwist m).conjF p = hs.conjF (p + m)

The conjugate filtration of a Tate twist is translated by the same amount.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.tateTwist_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m p : ℤ) : (hs.tateTwist m).piece p = hs.piece (p + m)

The p-th Hodge component of V(m) is the (p+m)-th component of V.

@[simp]

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

The Hodge numbers of a Tate twist are translated by m.

theorem TauCeti.Hodge.HodgeStructureOn.isEffective_tateTwist_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m : ℤ) : (hs.tateTwist m).IsEffective ↔ hs.F m = ⊤

A Tate twist is effective exactly when its translated zeroth filtration step is the whole space. This is not a simp lemma: with HodgeStructureOn.isEffective_iff and HodgeStructureOn.tateTwist_F tagged, simp already normalizes the left-hand side.

theorem TauCeti.Hodge.HodgeStructureOn.isEffective_tateTwist_iff_F_eq_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (m : ℤ) : (hs.tateTwist m).IsEffective ↔ hs.F (n + 1 - m) = ⊥

Equivalently, a Tate twist is effective exactly when the translated filtration vanishes one step above its new weight.

noncomputable def TauCeti.Hodge.HodgeStructure.Hom.tateTwist {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂} {n : ℤ} {source : HodgeStructure h₁ n} {target : HodgeStructure h₂ n} (f : source.Hom target) (m : ℤ) : Hom (HodgeStructureOn.tateTwist source m) (HodgeStructureOn.tateTwist target m)

A Hodge morphism induces a morphism between the same Tate twists of its source and target.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.Hom.tateTwist_toIntLinearMap {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂} {n : ℤ} {source : HodgeStructure h₁ n} {target : HodgeStructure h₂ n} (f : source.Hom target) (m : ℤ) : (f.tateTwist m).toIntLinearMap = f.toIntLinearMap

Twisting a morphism does not change its underlying integral linear map.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.Hom.tateTwist_apply {V₁ : Type u₁} {V₂ : Type u₂} {W₁ : Type v₁} {W₂ : Type v₂} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂} {n : ℤ} {source : HodgeStructure h₁ n} {target : HodgeStructure h₂ n} (f : source.Hom target) (m : ℤ) (x : W₁) : (f.tateTwist m).toLinearMap x = f.toLinearMap x

Twisting a morphism does not change its action on the complexification.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.Hom.tateTwist_id {V₁ : Type u₁} {W₁ : Type v₁} [AddCommGroup V₁] [AddCommGroup W₁] [Module ℂ W₁] {ι₁ : V₁ →ₗ[ℤ] W₁} {h₁ : IsBaseChange ℂ ι₁} {n : ℤ} (source : HodgeStructure h₁ n) (m : ℤ) : (id source).tateTwist m = id (HodgeStructureOn.tateTwist source m)

Tate twist preserves identity morphisms.

@[simp]

theorem TauCeti.Hodge.HodgeStructure.Hom.tateTwist_comp {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} {W₁ : Type v₁} {W₂ : Type v₂} {W₃ : Type v₃} [AddCommGroup V₁] [AddCommGroup V₂] [AddCommGroup V₃] [AddCommGroup W₁] [Module ℂ W₁] [AddCommGroup W₂] [Module ℂ W₂] [AddCommGroup W₃] [Module ℂ W₃] {ι₁ : V₁ →ₗ[ℤ] W₁} {ι₂ : V₂ →ₗ[ℤ] W₂} {ι₃ : V₃ →ₗ[ℤ] W₃} {h₁ : IsBaseChange ℂ ι₁} {h₂ : IsBaseChange ℂ ι₂} {h₃ : IsBaseChange ℂ ι₃} {n : ℤ} {source : HodgeStructure h₁ n} {target : HodgeStructure h₂ n} {third : HodgeStructure h₃ n} (g : target.Hom third) (f : source.Hom target) (m : ℤ) : (g.comp f).tateTwist m = (g.tateTwist m).comp (f.tateTwist m)

Tate twist preserves composition of Hodge morphisms.

theorem TauCeti.Hodge.IsPolarization.tateTwist {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (hQ : IsPolarization hℂ hs Q) (m : ℤ) : IsPolarization hℂ (HodgeStructureOn.tateTwist hs m) Q

A form polarizing a pure Hodge structure also polarizes each of its Tate twists.

theorem TauCeti.Hodge.IsPolarization.of_F_eq_F_add {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (hQ : IsPolarization hℂ hs Q) {n' : ℤ} {hs' : HodgeStructure hℂ n'} (m : ℤ) (hn : n' = n - 2 * m) (hF : ∀ (p : ℤ), hs'.F p = hs.F (p + m)) : IsPolarization hℂ hs' Q

A form polarizing a pure Hodge structure also polarizes every Hodge structure on the same complex vector space whose filtration is a translate of the original one by m, provided its weight is n - 2m. Such a structure is the Tate twist by m up to the identification of the propositionally equal weights.

def TauCeti.Hodge.Polarization.tateTwist {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (m : ℤ) : Polarization hℂ (HodgeStructureOn.tateTwist hs m)

The polarization of a Tate twist obtained from a polarization of the original structure.

@[simp]

theorem TauCeti.Hodge.Polarization.tateTwist_Qint {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (m : ℤ) : (P.tateTwist m).Qint = P.Qint

Tate twisting a polarization leaves its integral form unchanged.

@[simp]

theorem TauCeti.Hodge.Polarization.tateTwist_Q {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (m : ℤ) : (P.tateTwist m).Q = P.Q

Tate twisting a polarization leaves its complex form unchanged.

theorem TauCeti.Hodge.IsPolarizable.tateTwist {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (h : IsPolarizable hℂ hs) (m : ℤ) : IsPolarizable hℂ (HodgeStructureOn.tateTwist hs m)

Every Tate twist of a polarizable Hodge structure is polarizable.