The pure Hodge structure on a complex graded piece

The purity axiom of a mixed Hodge structure is imposed on the rational graded pieces: the complexification ℂ ⊗[ℚ] grᵂ_k of grᵂ_k = W_k / W_{k-1} carries a pure Hodge structure of weight k. The mixed theory itself, however, runs inside the complex model: Deligne's bigrading I^{p,q} is built from the Hodge filtration F, its conjugate, and the complexified weight filtration WC, and its elements are compared with the Hodge components of WC_k / WC_{k-1}. This file moves the pure structure from the first model to the second.

The transport is the identification TauCeti.Hodge.gradedComplexEquiv, and what makes it legitimate is that this identification intertwines the two conjugations (TauCeti.Hodge.gradedComplexEquiv_latticeConj): the canonical conjugation of a complexified rational space on the left, and on the right the conjugation that lattice conjugation induces on the complex graded piece, each step of WC being the complexification of a rational subspace and therefore conjugation-stable.

Main declarations

• TauCeti.Hodge.MixedHodgeStructure.gradedConjugation: the conjugation induced by lattice conjugation on the k-th complex graded piece.
• TauCeti.Hodge.MixedHodgeStructure.complexGradedHodgeStructure: the pure Hodge structure of weight k carried by WC_k / WC_{k-1}, with its filtration TauCeti.Hodge.complexGradedF and its Hodge components computed.
• TauCeti.Hodge.MixedHodgeStructure.isInternal_complexGradedHodgeStructure_piece: the Hodge decomposition of a complex graded piece.
• TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_piece: a vector of W_k that lies in F^p and lies in conj F^{k-p} modulo W_{k-1} has its class in the Hodge component H^{p,k-p} of the graded piece. This is the form in which the pieces of Deligne's bigrading meet the graded Hodge structure, and TauCeti.Hodge.MixedHodgeStructure.mem_complexGradedHodgeStructure_piece_iff shows the criterion is exact. TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_F and its conjugate analogue are the corresponding criteria for the two induced filtrations.

References

The graded-piece comparison and the bidegree bookkeeping follow Peters–Steenbrink, Mixed Hodge Structures, Ch. 3, and Deligne, Théorie de Hodge II, §1.2.1 and 1.2.10.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.gradedConjugation {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) : Conjugation (weightGradedComplex mhs.WC k)

The conjugation induced by lattice conjugation on the k-th graded piece of the complexified weight filtration.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.gradedConjugation_mk {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) (x : ↥(mhs.WC k)) : (mhs.gradedConjugation k).toEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(latticeConj hℂ) ↑x, ⋯⟩

The induced conjugation acts on a class through lattice conjugation of a representative.

theorem TauCeti.Hodge.MixedHodgeStructure.gradedComplexEquiv_gradedConjugation {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) (x : TensorProduct ℚ ℂ (weightGradedRat mhs.WQ k)) : (gradedComplexEquiv hℚ hℂ mhs.WQ ⋯ k) ((latticeConj ⋯) x) = (mhs.gradedConjugation k).toEquiv ((gradedComplexEquiv hℚ hℂ mhs.WQ ⋯ k) x)

The comparison of the rational and complex models of the k-th graded piece intertwines the canonical conjugation of the former with the induced conjugation of the latter.

theorem TauCeti.Hodge.MixedHodgeStructure.gradedComplexEquiv_symm_gradedConjugation {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) (y : weightGradedComplex mhs.WC k) : (gradedComplexEquiv hℚ hℂ mhs.WQ ⋯ k).symm ((mhs.gradedConjugation k).toEquiv y) = (latticeConjugation ⋯).toEquiv ((gradedComplexEquiv hℚ hℂ mhs.WQ ⋯ k).symm y)

The inverse comparison intertwines the conjugations, in the form the transport of a Hodge structure consumes.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.complexGradedHodgeStructure {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) : HodgeStructureOn (weightGradedComplex mhs.WC k) (mhs.gradedConjugation k) k

The k-th complex graded piece of a mixed Hodge structure is a pure Hodge structure of weight k. Its conjugation is the one lattice conjugation induces on WC_k / WC_{k-1}, and its filtration is the one the Hodge filtration induces there; purity is transported from the rational graded piece along TauCeti.Hodge.gradedComplexEquiv, which is legitimate because that identification intertwines the conjugations.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.complexGradedHodgeStructure_F {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) : (mhs.complexGradedHodgeStructure k).F p = complexGradedF mhs.WC mhs.F k p

The filtration of the graded pure structure is the filtration induced by F on the complex graded piece, on the nose.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.complexGradedHodgeStructure_conjF {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) : (mhs.complexGradedHodgeStructure k).conjF p = complexGradedF mhs.WC (fun (q : ℤ) => Submodule.map (latticeConj hℂ) (mhs.F q)) k p

The conjugate filtration of the graded pure structure is the filtration induced by the conjugate of F.

theorem TauCeti.Hodge.MixedHodgeStructure.complexGradedHodgeStructure_piece {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) : (mhs.complexGradedHodgeStructure k).piece p = complexGradedF mhs.WC mhs.F k p ⊓ complexGradedF mhs.WC (fun (q : ℤ) => Submodule.map (latticeConj hℂ) (mhs.F q)) k (k - p)

The Hodge components of the graded pure structure, spelled out in terms of the Hodge filtration and its conjugate.

theorem TauCeti.Hodge.MixedHodgeStructure.map_gradedHodgeStructure_piece {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) : Submodule.map (↑(gradedComplexEquiv hℚ hℂ mhs.WQ ⋯ k)) (HodgeStructureOn.piece (mhs.gradedHodgeStructure k) p) = (mhs.complexGradedHodgeStructure k).piece p

The comparison of the two models of a graded piece carries Hodge components to Hodge components.

theorem TauCeti.Hodge.MixedHodgeStructure.isInternal_complexGradedHodgeStructure_piece {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k : ℤ) : DirectSum.IsInternal (mhs.complexGradedHodgeStructure k).piece

The Hodge decomposition of a complex graded piece: the Hodge components of WC_k / WC_{k-1} are an internal direct sum.

theorem TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_F {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) (y : ↥(mhs.WC k)) (hF : ↑y ∈ mhs.F p) : Submodule.Quotient.mk y ∈ (mhs.complexGradedHodgeStructure k).F p

A vector of W_k lying in F^p has its class in the p-th step of the filtration induced on the graded piece.

theorem TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_conjF {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) (y : ↥(mhs.WC k)) (hF : ↑y ∈ mhs.conjF p) : Submodule.Quotient.mk y ∈ (mhs.complexGradedHodgeStructure k).conjF p

A vector of W_k lying in conj F^p has its class in the p-th step of the conjugate filtration induced on the graded piece.

theorem TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_piece {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) (y : ↥(mhs.WC k)) (hF : ↑y ∈ mhs.F p) (hconj : ↑y ∈ Submodule.map (latticeConj hℂ) (mhs.F (k - p)) ⊔ mhs.WC (k - 1)) : Submodule.Quotient.mk y ∈ (mhs.complexGradedHodgeStructure k).piece p

A representative criterion for the Hodge components of a complex graded piece. A vector of W_k that lies in F^p, and that lies in the conjugate conj F^{k-p} modulo W_{k-1}, has its class in the Hodge component H^{p,k-p} of the graded piece.

The second hypothesis is weaker than membership of conj F^{k-p}, and the weakening is what makes the criterion usable: in the mixed theory the conjugation relations hold only modulo lower steps of the weight filtration, which is exactly the shape in which the pieces of Deligne's bigrading I^{p,q} present themselves.

theorem TauCeti.Hodge.MixedHodgeStructure.mem_complexGradedHodgeStructure_piece_iff {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} (mhs : MixedHodgeStructure hℚ hℂ) (k p : ℤ) (u : weightGradedComplex mhs.WC k) : u ∈ (mhs.complexGradedHodgeStructure k).piece p ↔ ∃ (y : ↥(mhs.WC k)), ↑y ∈ mhs.F p ∧ ↑y ∈ Submodule.map (latticeConj hℂ) (mhs.F (k - p)) ⊔ mhs.WC (k - 1) ∧ Submodule.Quotient.mk y = u

The Hodge components of a complex graded piece, by representatives. A class lies in the component H^{p,k-p} exactly when it has a representative in W_k that lies in F^p and lies in conj F^{k-p} modulo W_{k-1}.

The forward direction is what turns a statement about the graded piece back into one about representatives in W_k; the backward direction is TauCeti.Hodge.MixedHodgeStructure.mk_mem_complexGradedHodgeStructure_piece.