Tate Hodge structures

The Tate structure ℤ(m) is the rank-one pure Hodge structure of weight -2m and type (-m,-m). Its complexification is ℂ, with the integral lattice embedded by the usual map ℤ → ℂ; its decreasing filtration is the whole line through degree -m and zero above it.

This is the first concrete nonzero inhabitant of TauCeti.Hodge.HodgeStructure. Besides fixing the weight and filtration-shift conventions needed by later Tate twists, it verifies directly that the opposed-filtration definition has the intended rank-one objects. Multiplication of integers polarizes it, so it also witnesses that the Hodge–Riemann relations are satisfiable.

The convention follows the Hodge structures roadmap and standard Hodge-theory notation; see Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.

Main declarations

• TauCeti.Hodge.tate: the Tate Hodge structure ℤ(m) of weight -2m.
• TauCeti.Hodge.tate_F: its filtration is ⊤ exactly in degrees at most -m.
• TauCeti.Hodge.tate_piece: its only nonzero Hodge component has bidegree (-m,-m).
• TauCeti.Hodge.finrank_tate_piece: its Hodge number there is one and all others are zero.
• TauCeti.Hodge.tateHodgeType: the numerical Hodge type of ℤ(m), effective exactly when m ≤ 0 (TauCeti.Hodge.tateHodgeType_isEffective_iff).
• TauCeti.Hodge.isPolarization_tate: multiplication of integers satisfies the Hodge–Riemann relations for it, and TauCeti.Hodge.tatePolarization bundles that as a polarization.

@[reducible, inline]

abbrev TauCeti.Hodge.tateLatticeMap : ℤ →ₗ[ℤ] ℂ

The integral lattice map ℤ → ℂ used by the Tate Hodge structure.

theorem TauCeti.Hodge.isBaseChange_tateLatticeMap : IsBaseChange ℂ tateLatticeMap

The usual inclusion ℤ → ℂ exhibits ℂ as the complexification of the rank-one lattice.

noncomputable def TauCeti.Hodge.tate (m : ℤ) : HodgeStructure isBaseChange_tateLatticeMap (-2 * m)

The Tate Hodge structure ℤ(m), of weight -2m and Hodge type (-m,-m).

@[simp]

theorem TauCeti.Hodge.tate_F (m p : ℤ) : (tate m).F p = if p ≤ -m then ⊤ else ⊥

The Hodge filtration of ℤ(m) is the whole line exactly through degree -m.

theorem TauCeti.Hodge.tate_isEffective_iff (m : ℤ) : HodgeStructureOn.IsEffective (tate m) ↔ m ≤ 0

The Tate Hodge structure is effective exactly when m ≤ 0. This is not a simp lemma: with HodgeStructureOn.isEffective_iff tagged, simp already normalizes the left-hand side.

@[simp]

theorem TauCeti.Hodge.tate_piece (m p : ℤ) : HodgeStructureOn.piece (tate m) p = if p = -m then ⊤ else ⊥

The only nonzero Hodge component of ℤ(m) is H^{-m,-m}.

@[simp]

theorem TauCeti.Hodge.finrank_tate_piece (m p : ℤ) : Module.finrank ℂ ↥(HodgeStructureOn.piece (tate m) p) = if p = -m then 1 else 0

The Hodge number of ℤ(m) is one in bidegree (-m,-m) and zero elsewhere.

The numerical type of a Tate structure

def TauCeti.Hodge.tateHodgeType (m : ℤ) : HodgeType

The Hodge type of the Tate structure ℤ(m): weight -2m, with h^{-m,-m} = 1 and every other Hodge number zero.

@[simp]

theorem TauCeti.Hodge.tateHodgeType_weight (m : ℤ) : (tateHodgeType m).weight = -2 * m

@[simp]

theorem TauCeti.Hodge.tateHodgeType_h (m p : ℤ) : (tateHodgeType m).h p = if p = -m then 1 else 0

@[simp]

theorem TauCeti.Hodge.tate_hodgeNumber (m p : ℤ) : HodgeStructureOn.hodgeNumber (tate m) p = if p = -m then 1 else 0

The Hodge numbers of the Tate structure ℤ(m): one in bidegree (-m,-m), zero elsewhere.

@[simp]

theorem TauCeti.Hodge.tate_hodgeType (m : ℤ) : HodgeStructureOn.hodgeType (tate m) = tateHodgeType m

The Hodge type of the Tate structure ℤ(m) is the prescribed one.

@[simp]

theorem TauCeti.Hodge.tateHodgeType_isEffective_iff (m : ℤ) : (tateHodgeType m).IsEffective ↔ m ≤ 0

The Hodge type of ℤ(m) is effective exactly when m ≤ 0.

theorem TauCeti.Hodge.finsum_tateHodgeType_h_eq_one (m : ℤ) : ∑ᶠ (p : ℤ), (tateHodgeType m).h p = 1

The single Hodge number of ℤ(m) accounts for the whole rank-one lattice.

The polarization of a Tate structure

theorem TauCeti.Hodge.latticeConj_tateLatticeMap (z : ℂ) : (latticeConj isBaseChange_tateLatticeMap) z = (starRingEnd ℂ) z

The conjugation of the Tate complexification is complex conjugation.

theorem TauCeti.Hodge.bilinForm_tateLatticeMap_mul : isBaseChange_tateLatticeMap.bilinForm (LinearMap.mul ℤ ℤ) = LinearMap.mul ℂ ℂ

The complexification of integer multiplication is complex multiplication.

theorem TauCeti.Hodge.isPolarization_tate (m : ℤ) : IsPolarization isBaseChange_tateLatticeMap (tate m) (LinearMap.mul ℤ ℤ)

Multiplication of integers satisfies the Hodge–Riemann relations for ℤ(m).

def TauCeti.Hodge.tatePolarization (m : ℤ) : Polarization isBaseChange_tateLatticeMap (tate m)

The Tate Hodge structure ℤ(m), polarized by multiplication of integers.

@[simp]

theorem TauCeti.Hodge.tatePolarization_Q (m : ℤ) : (tatePolarization m).Q = LinearMap.mul ℂ ℂ

The complex form of the Tate polarization is multiplication on the complex line.

theorem TauCeti.Hodge.isPolarizable_tate (m : ℤ) : IsPolarizable isBaseChange_tateLatticeMap (tate m)

The Tate Hodge structure is polarizable.