Mixed Hodge structures from a bigrading

Deligne's theorem (TauCeti.Hodge.MixedHodgeStructure.isInternal_deligneSplittingFamily) says that a mixed Hodge structure carries a bigrading I^{p,q} of its complex model from which both filtrations are read off,

W_k = ⨆_{p + q ≤ k} I^{p,q}, F^p = ⨆_{p' ≥ p} I^{p',q'},

and whose pieces are conjugate to each other modulo lower weight. This file proves the converse: a rational weight filtration and a Hodge filtration admitting such a bigrading form a mixed Hodge structure. The conjugation condition used here, conj I^{p,q} ≤ I^{q,p} ⊔ W_{p+q-1} — the images of I^{p,q} and I^{q,p} in grᵂ_{p+q} are conjugate — is weaker than Deligne's and suffices for the converse, and the bigrading need not be Deligne's own: no uniqueness is claimed or needed.

The converse is a way to recognise new mixed Hodge structures. Verifying purity of every graded piece directly means computing induced filtrations on quotients, whereas exhibiting a bigrading is a statement about subspaces of the ambient complex space alone. Together with Deligne's theorem it characterises mixed Hodge structures among bounded pairs of filtrations (TauCeti.Hodge.MixedHodgeStructure.exists_isHodgeBigrading_iff).

The argument takes place in the ambient space. On grᵂ_k, the images of F^p and of conj F^{k+1-p} are complementary: modulo W_{k-1}, the first is spanned by the pieces I^{p',q'} of total degree k with p' ≥ p, the second is contained in the span of those with q' ≥ k + 1 - p, and independence of the bigrading separates the two sets of bidegrees, while every piece of total degree k lies in one of the two spans.

Main declarations

• TauCeti.Hodge.IsHodgeBigrading: a bigrading of the complex model adapted to a rational weight filtration and a Hodge filtration.
• TauCeti.Hodge.IsHodgeBigrading.isCompl_complexGradedF: the induced filtration on a complex graded piece is opposed to its conjugate.
• TauCeti.Hodge.MixedHodgeStructure.ofIsHodgeBigrading: the mixed Hodge structure defined by a bounded pair of filtrations with a bigrading.
• TauCeti.Hodge.MixedHodgeStructure.isHodgeBigrading_deligneSplittingFamily: Deligne's bigrading is such a bigrading.
• TauCeti.Hodge.MixedHodgeStructure.exists_isHodgeBigrading_iff: a bounded pair of filtrations satisfies the purity axiom exactly when it admits a bigrading.

References

Deligne, Théorie de Hodge II, 1.2.8 and 1.2.10; Peters–Steenbrink, Mixed Hodge Structures, Lemma-Definition 3.4 and Ch. 3.1, where mixed Hodge structures are characterised by their bigradings.

structure TauCeti.Hodge.IsHodgeBigrading {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 ℂ ιℂ) (WQ : ℤ → Submodule ℚ Vℚ) (F : ℤ → Submodule ℂ Vℂ) (I : ℤ × ℤ → Submodule ℂ Vℂ) : Prop

A Hodge bigrading for a rational weight filtration WQ and a Hodge filtration F: an independent family I^{p,q} of complex subspaces recovering the complexified weight filtration as W_k = ⨆_{p+q ≤ k} I^{p,q} and the Hodge filtration as F^p = ⨆_{p' ≥ p} I^{p',q'}, whose pieces are conjugate modulo lower weight: conj I^{p,q} ≤ I^{q,p} ⊔ W_{p+q-1}.

• iSupIndep : _root_.iSupIndep I

  The pieces of the bigrading are independent.

• rationalToComplexSubmodule_eq_iSup (k : ℤ) : rationalToComplexSubmodule hℚ hℂ (WQ k) = ⨆ (pq : ℤ × ℤ), ⨆ (_ : pq.1 + pq.2 ≤ k), I pq

  The complexified weight filtration is the sum of the pieces of bounded total degree.

• F_eq_iSup (p : ℤ) : F p = ⨆ (pq : ℤ × ℤ), ⨆ (_ : p ≤ pq.1), I pq

  The Hodge filtration is the sum of the pieces of bounded-below first index.

• map_latticeConj_le (pq : ℤ × ℤ) : Submodule.map (latticeConj hℂ) (I pq) ≤ I pq.swap ⊔ rationalToComplexSubmodule hℚ hℂ (WQ (pq.1 + pq.2 - 1))

  Conjugation exchanges the pieces I^{p,q} and I^{q,p} modulo lower weight.

theorem TauCeti.Hodge.IsHodgeBigrading.prod {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {V'ℤ : Type u_1} {V'ℚ : Type u_2} {V'ℂ : Type u_3} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℚ : IsBaseChange ℚ ι'ℚ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {W : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {W' : ℤ → Submodule ℚ V'ℚ} {F' : ℤ → Submodule ℂ V'ℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} {I' : ℤ × ℤ → Submodule ℂ V'ℂ} (h : IsHodgeBigrading hℚ hℂ W F I) (h' : IsHodgeBigrading h'ℚ h'ℂ W' F' I') : IsHodgeBigrading ⋯ ⋯ (fun (k : ℤ) => (W k).prod (W' k)) (fun (p : ℤ) => (F p).prod (F' p)) fun (pq : ℤ × ℤ) => (I pq).prod (I' pq)

Products of Hodge bigradings are Hodge bigradings for the product filtrations.

theorem TauCeti.Hodge.IsHodgeBigrading.le_rationalToComplexSubmodule {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) {pq : ℤ × ℤ} {k : ℤ} (hk : pq.1 + pq.2 ≤ k) : I pq ≤ rationalToComplexSubmodule hℚ hℂ (WQ k)

A piece of a Hodge bigrading lies in the weight step of its total degree.

theorem TauCeti.Hodge.IsHodgeBigrading.le_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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) {pq : ℤ × ℤ} {p : ℤ} (hp : p ≤ pq.1) : I pq ≤ F p

A piece of a Hodge bigrading lies in the Hodge step of its first index.

theorem TauCeti.Hodge.IsHodgeBigrading.monotone {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) : Monotone WQ

A weight filtration admitting a Hodge bigrading is increasing.

theorem TauCeti.Hodge.IsHodgeBigrading.antitone {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) : Antitone F

A Hodge filtration admitting a Hodge bigrading is decreasing.

theorem TauCeti.Hodge.IsHodgeBigrading.le_map_latticeConj_sup {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (pq : ℤ × ℤ) : I pq ≤ Submodule.map (latticeConj hℂ) (I pq.swap) ⊔ rationalToComplexSubmodule hℚ hℂ (WQ (pq.1 + pq.2 - 1))

Every piece of a Hodge bigrading lies in the conjugate of the swapped piece, modulo lower weight.

theorem TauCeti.Hodge.IsHodgeBigrading.F_inf_rationalToComplexSubmodule_eq_iSup {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (p k : ℤ) : F p ⊓ rationalToComplexSubmodule hℚ hℂ (WQ k) = ⨆ (pq : ℤ × ℤ), ⨆ (_ : p ≤ pq.1 ∧ pq.1 + pq.2 ≤ k), I pq

A Hodge step meets a weight step in the sum of the pieces lying in both.

theorem TauCeti.Hodge.IsHodgeBigrading.map_latticeConj_F_inf_rationalToComplexSubmodule_le_iSup {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (r k : ℤ) : Submodule.map (latticeConj hℂ) (F r) ⊓ rationalToComplexSubmodule hℚ hℂ (WQ k) ≤ ⨆ (pq : ℤ × ℤ), ⨆ (_ : pq.1 + pq.2 ≤ k - 1 ∨ r ≤ pq.2), I pq

Inside W_k, the conjugate of the Hodge step F^r is spanned, modulo W_{k-1}, by pieces whose second index is at least r.

theorem TauCeti.Hodge.IsHodgeBigrading.isCompl_complexGradedF {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (k p : ℤ) : IsCompl (complexGradedF (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ j)) F k p) (complexGradedF (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ j)) (fun (q : ℤ) => Submodule.map (latticeConj hℂ) (F q)) k (k + 1 - p))

The filtration induced on a complex graded piece is opposed to its conjugate. On grᵂ_k, the images of F^p and of conj F^{k+1-p} are complementary.

theorem TauCeti.Hodge.IsHodgeBigrading.exists_hodgeStructure_F_eq_gradedF {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (hF : ∃ (p : ℤ), F p = ⊤) (k : ℤ) : ∃ (hs : HodgeStructure ⋯ k), hs.F = gradedF hℚ hℂ WQ ⋯ F k

Purity of the graded pieces. If a Hodge filtration with a Hodge bigrading is exhaustive, then on every rational graded piece grᵂ_k the induced filtration is the Hodge filtration of a pure Hodge structure of weight k: this is the purity axiom of a mixed Hodge structure.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.ofIsHodgeBigrading {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (hW_top : ∃ (k : ℤ), WQ k = ⊤) (hW_bot : ∃ (k : ℤ), WQ k = ⊥) (hF_top : ∃ (p : ℤ), F p = ⊤) (hF_bot : ∃ (p : ℤ), F p = ⊥) : MixedHodgeStructure hℚ hℂ

The mixed Hodge structure defined by a bigrading. A bounded rational weight filtration and a bounded Hodge filtration admitting a Hodge bigrading form a mixed Hodge structure.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.ofIsHodgeBigrading_WQ {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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (hW_top : ∃ (k : ℤ), WQ k = ⊤) (hW_bot : ∃ (k : ℤ), WQ k = ⊥) (hF_top : ∃ (p : ℤ), F p = ⊤) (hF_bot : ∃ (p : ℤ), F p = ⊥) : (ofIsHodgeBigrading h hW_top hW_bot hF_top hF_bot).WQ = WQ

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.ofIsHodgeBigrading_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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} {I : ℤ × ℤ → Submodule ℂ Vℂ} (h : IsHodgeBigrading hℚ hℂ WQ F I) (hW_top : ∃ (k : ℤ), WQ k = ⊤) (hW_bot : ∃ (k : ℤ), WQ k = ⊥) (hF_top : ∃ (p : ℤ), F p = ⊤) (hF_bot : ∃ (p : ℤ), F p = ⊥) : (ofIsHodgeBigrading h hW_top hW_bot hF_top hF_bot).F = F

theorem TauCeti.Hodge.MixedHodgeStructure.isHodgeBigrading_deligneSplittingFamily {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ℂ) : IsHodgeBigrading hℚ hℂ mhs.WQ mhs.F mhs.deligneSplittingFamily

Deligne's bigrading is a Hodge bigrading of the filtrations of a mixed Hodge structure.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.ofIsHodgeBigrading_deligneSplittingFamily {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ℂ) : ofIsHodgeBigrading ⋯ ⋯ ⋯ ⋯ ⋯ = mhs

Rebuilding a mixed Hodge structure from Deligne's bigrading returns it.

theorem TauCeti.Hodge.MixedHodgeStructure.exists_isHodgeBigrading_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 ℂ ιℂ} {WQ : ℤ → Submodule ℚ Vℚ} {F : ℤ → Submodule ℂ Vℂ} (hWQ : Monotone WQ) (hW_top : ∃ (k : ℤ), WQ k = ⊤) (hW_bot : ∃ (k : ℤ), WQ k = ⊥) (hF_anti : Antitone F) (hF_top : ∃ (p : ℤ), F p = ⊤) (hF_bot : ∃ (p : ℤ), F p = ⊥) : (∃ (I : ℤ × ℤ → Submodule ℂ Vℂ), IsHodgeBigrading hℚ hℂ WQ F I) ↔ ∀ (k : ℤ), ∃ (hs : HodgeStructure ⋯ k), hs.F = gradedF hℚ hℂ WQ hWQ F k

A pair of bounded filtrations is a mixed Hodge structure exactly when it admits a Hodge bigrading. Precisely: the purity axiom holds for a bounded increasing rational weight filtration and a bounded decreasing Hodge filtration if and only if the two filtrations have a Hodge bigrading.