Pure Hodge structures

This file defines a pure Hodge structure of arbitrary integral weight on a complex vector space with a specified conjugation. The primary datum is a bounded decreasing filtration F; purity is the condition that F p and the conjugate of F (n + 1 - p) are complementary for every p.

Keeping the ambient conjugation as a parameter gives one definition for both integral and rational Hodge structures. TauCeti.Hodge.HodgeStructure specializes it to an abstract complexification of an integral module using the canonical lattice-induced conjugation. Finiteness and freeness of a lattice are imposed by the arithmetic results that use them, rather than being redundant parameters of this abbreviation.

The opposed-filtration convention follows Deligne, Théorie de Hodge II, §1.2.1. It is the convention fixed by the Hodge structures roadmap and by the #mathlib4 discussion Complexifications with a view towards Hodge theory involving Johan Commelin, Andrew Yang, Kevin Buzzard, and Joël Riou.

Main declarations

• TauCeti.Hodge.HodgeStructureOn: a bounded n-opposed decreasing filtration on a complex vector space with conjugation.
• TauCeti.Hodge.HodgeStructure: the specialization to the canonical conjugation of an integral complexification.
• TauCeti.Hodge.HodgeStructureOn.piece: the Hodge component H^{p,n-p}.
• TauCeti.Hodge.HodgeStructureOn.conj_piece: conjugation exchanges H^{p,n-p} and H^{n-p,p}, with TauCeti.Hodge.HodgeStructureOn.conj_mem_piece its elementwise form and TauCeti.Hodge.HodgeStructureOn.pieceConjEquiv its packaging as a real-linear isomorphism.
• TauCeti.Hodge.HodgeStructureOn.finite_setOf_piece_ne_bot: only finitely many Hodge components are nonzero, because the filtration is bounded.
• TauCeti.Hodge.HodgeStructureOn.comap: transport of a Hodge structure along a linear equivalence intertwining the conjugations, with the transport of its Hodge components TauCeti.Hodge.HodgeStructureOn.comap_piece.
• TauCeti.Hodge.HodgeStructureOn.IsEffective: the filtration is supported in bidegrees with both indices nonnegative, with TauCeti.Hodge.HodgeStructureOn.IsEffective.piece_weight_eq_F identifying the Hodge component in the degree of the weight with the filtration step there.

structure TauCeti.Hodge.HodgeStructureOn (W : Type u) [AddCommGroup W] [Module ℂ W] (ω : Conjugation W) (n : ℤ) : Type u

A pure Hodge structure of weight n on a complex vector space with conjugation ω.

The decreasing filtration F is bounded and n-opposed to its conjugate: for every p, F p is complementary to the conjugate of F (n + 1 - p).

• F : ℤ → Submodule ℂ W

  The decreasing Hodge filtration.

• F_antitone : Antitone self.F

  The Hodge filtration is decreasing.

• F_top : ∃ (p : ℤ), self.F p = ⊤

  The filtration is exhaustive: some step is the whole space.

• opposed (p : ℤ) : IsCompl (self.F p) (Submodule.map (↑ω.toEquiv) (self.F (n + 1 - p)))

  The filtration is opposed to its conjugate in weight n.

theorem TauCeti.Hodge.HodgeStructureOn.ext_iff {W : Type u} {inst✝ : AddCommGroup W} {inst✝¹ : Module ℂ W} {ω : Conjugation W} {n : ℤ} {x y : HodgeStructureOn W ω n} : x = y ↔ x.F = y.F

theorem TauCeti.Hodge.HodgeStructureOn.ext {W : Type u} {inst✝ : AddCommGroup W} {inst✝¹ : Module ℂ W} {ω : Conjugation W} {n : ℤ} {x y : HodgeStructureOn W ω n} (F : x.F = y.F) : x = y

@[reducible, inline]

abbrev TauCeti.Hodge.HodgeStructure {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (n : ℤ) : Type v

The specialization of a pure Hodge structure to an abelian group with an arbitrary abstract complexification. Its conjugation is induced canonically by the abelian group.

noncomputable def TauCeti.Hodge.HodgeStructureOn.conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : Submodule ℂ W

The conjugate of the p-th step of the Hodge filtration.

theorem TauCeti.Hodge.HodgeStructureOn.conjF_def {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.conjF p = Submodule.map (↑ω.toEquiv) (hs.F p)

The conjugate filtration step is the image under the specified conjugation.

theorem TauCeti.Hodge.HodgeStructureOn.conjF_antitone {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : Antitone hs.conjF

The conjugate of the Hodge filtration is decreasing.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.mem_conjF_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (x : W) : x ∈ hs.conjF p ↔ ω.toEquiv x ∈ hs.F p

Membership in a conjugate filtration step is detected by applying the conjugation.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.conjF_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : Submodule.map (↑ω.toEquiv) (hs.conjF p) = hs.F p

Conjugating a filtration step twice recovers that step.

theorem TauCeti.Hodge.HodgeStructureOn.isCompl_F_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : IsCompl (hs.F p) (hs.conjF (n + 1 - p))

Opposedness expressed using conjF.

theorem TauCeti.Hodge.HodgeStructureOn.F_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : ∃ (p : ℤ), hs.F p = ⊥

The Hodge filtration is separated: some step is zero.

theorem TauCeti.Hodge.HodgeStructureOn.F_eq_top_of_le {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} (hq : hs.F q = ⊤) (hpq : p ≤ q) : hs.F p = ⊤

At every index below a top step, the decreasing filtration is also the whole space.

theorem TauCeti.Hodge.HodgeStructureOn.F_eq_bot_of_le {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p q : ℤ} (hp : hs.F p = ⊥) (hpq : p ≤ q) : hs.F q = ⊥

At every index above a bottom step, the decreasing filtration is also zero.

theorem TauCeti.Hodge.HodgeStructureOn.exists_forall_le_F_eq_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : ∃ (q : ℤ), ∀ p ≤ q, hs.F p = ⊤

Exhaustiveness holds uniformly below a suitable filtration index.

theorem TauCeti.Hodge.HodgeStructureOn.exists_forall_F_eq_bot_of_le {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : ∃ (p : ℤ), ∀ (q : ℤ), p ≤ q → hs.F q = ⊥

Separatedness holds uniformly above a suitable filtration index.

noncomputable def TauCeti.Hodge.HodgeStructureOn.piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : Submodule ℂ W

The Hodge component H^{p,n-p} = F^p ∩ overline{F^{n-p}}.

theorem TauCeti.Hodge.HodgeStructureOn.piece_def {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.piece p = hs.F p ⊓ hs.conjF (n - p)

The p-th Hodge component is the intersection of F p with the conjugate of F (n - p).

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.mem_piece_iff {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (x : W) : x ∈ hs.piece p ↔ x ∈ hs.F p ∧ x ∈ hs.conjF (n - p)

Membership in a Hodge component is membership in both defining filtration steps.

theorem TauCeti.Hodge.HodgeStructureOn.mem_piece_iff_of_conj_eq {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) {x : W} (hx : ω.toEquiv x = x) : x ∈ hs.piece p ↔ x ∈ hs.F p ∧ x ∈ hs.F (n - p)

A vector fixed by the conjugation lies in the Hodge component H^{p,n-p} exactly when it lies in the two filtration steps F^p and F^{n-p}.

theorem TauCeti.Hodge.HodgeStructureOn.piece_le_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.piece p ≤ hs.F p

A Hodge component lies in its corresponding filtration step.

theorem TauCeti.Hodge.HodgeStructureOn.piece_le_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : hs.piece p ≤ hs.conjF (n - p)

A Hodge component lies in the conjugate filtration step of complementary index.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.conj_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : Submodule.map (↑ω.toEquiv) (hs.piece p) = hs.piece (n - p)

Conjugation exchanges the Hodge components H^{p,n-p} and H^{n-p,p}.

theorem TauCeti.Hodge.HodgeStructureOn.conj_mem_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {p : ℤ} {x : W} (hx : x ∈ hs.piece p) : ω.toEquiv x ∈ hs.piece (n - p)

Elementwise form of the exchange of Hodge components by conjugation.

theorem TauCeti.Hodge.HodgeStructureOn.piece_eq_bot_of_F_eq_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {a p : ℤ} (ha : hs.F a = ⊤) (hp : p < a) : hs.piece p = ⊥

Below a filtration index at which a Hodge filtration is the whole space, every Hodge component vanishes: the conjugate step cutting it out is already zero.

theorem TauCeti.Hodge.HodgeStructureOn.piece_eq_bot_of_F_eq_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) {b p : ℤ} (hb : hs.F b = ⊥) (hp : b ≤ p) : hs.piece p = ⊥

Above a filtration index at which a Hodge filtration vanishes, every Hodge component vanishes.

theorem TauCeti.Hodge.HodgeStructureOn.finite_setOf_piece_ne_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : {p : ℤ | hs.piece p ≠ ⊥}.Finite

A bounded Hodge filtration has only finitely many nonzero Hodge components.

def TauCeti.Hodge.HodgeStructureOn.pieceConjEquiv {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) : ↥(hs.piece p) ≃ₗ[ℝ] ↥(hs.piece (n - p))

Conjugation restricts to a real-linear isomorphism from the Hodge component H^{p,n-p} onto its conjugate H^{n-p,p}. It is not complex-linear: it is conjugate-linear, so it is only an isomorphism after restricting scalars to ℝ.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.coe_pieceConjEquiv_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (x : ↥(hs.piece p)) : ↑((hs.pieceConjEquiv p) x) = ω.toEquiv ↑x

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.coe_pieceConjEquiv_symm_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (p : ℤ) (y : ↥(hs.piece (n - p))) : ↑((hs.pieceConjEquiv p).symm y) = ω.toEquiv ↑y

noncomputable def TauCeti.Hodge.HodgeStructureOn.comap {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {W' : Type u_1} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} (e : W ≃ₗ[ℂ] W') (he : ∀ (x : W), e (ω.toEquiv x) = ω'.toEquiv (e x)) (hs : HodgeStructureOn W' ω' n) : HodgeStructureOn W ω n

Pulling a Hodge structure back along a linear equivalence that intertwines the two conjugations. This is how a Hodge structure is transported between two models of the same complex vector space, for instance from a complexification to a graded piece identified with it.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.comap_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {W' : Type u_1} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} (e : W ≃ₗ[ℂ] W') (he : ∀ (x : W), e (ω.toEquiv x) = ω'.toEquiv (e x)) (hs : HodgeStructureOn W' ω' n) (p : ℤ) : (comap e he hs).F p = Submodule.comap (↑e) (hs.F p)

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.comap_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {W' : Type u_1} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} (e : W ≃ₗ[ℂ] W') (he : ∀ (x : W), e (ω.toEquiv x) = ω'.toEquiv (e x)) (hs : HodgeStructureOn W' ω' n) (p : ℤ) : (comap e he hs).conjF p = Submodule.comap (↑e) (hs.conjF p)

Transport along an equivalence intertwining the conjugations takes the conjugate filtration to the preimage of the conjugate filtration.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.comap_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {W' : Type u_1} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} (e : W ≃ₗ[ℂ] W') (he : ∀ (x : W), e (ω.toEquiv x) = ω'.toEquiv (e x)) (hs : HodgeStructureOn W' ω' n) (p : ℤ) : (comap e he hs).piece p = Submodule.comap (↑e) (hs.piece p)

Transport along an equivalence intertwining the conjugations takes each Hodge component to the preimage of the corresponding Hodge component.

def TauCeti.Hodge.HodgeStructureOn.IsEffective {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) : Prop

A weight-n Hodge structure is effective when its Hodge filtration begins at F 0 = ⊤. Equivalently, it ends at F (n + 1) = ⊥, and its Hodge components can occur only when both bidegrees are nonnegative.

@[simp]

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

Effectivity is the condition that the Hodge filtration begins at the whole space.

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

An effective Hodge filtration vanishes immediately above its weight.

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

Effectivity is equivalently the condition that the Hodge filtration vanishes immediately above its weight.

theorem TauCeti.Hodge.HodgeStructureOn.IsEffective.F_eq_top_of_nonpos {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} (h : hs.IsEffective) {p : ℤ} (hp : p ≤ 0) : hs.F p = ⊤

An effective Hodge filtration is the whole space in every nonpositive degree.

theorem TauCeti.Hodge.HodgeStructureOn.IsEffective.F_eq_bot_of_weight_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} (h : hs.IsEffective) {p : ℤ} (hp : n < p) : hs.F p = ⊥

An effective Hodge filtration vanishes in every degree strictly above its weight.

theorem TauCeti.Hodge.HodgeStructureOn.IsEffective.piece_weight_eq_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} (h : hs.IsEffective) : hs.piece n = hs.F n

In an effective Hodge structure the Hodge component in the degree of the weight is the filtration step of that degree: the conjugate step cutting it out is the conjugate of F 0 = ⊤, which is everything. Use it as an explicit rewrite rule.

theorem TauCeti.Hodge.HodgeStructureOn.IsEffective.piece_eq_bot_of_neg {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} (h : hs.IsEffective) {p : ℤ} (hp : p < 0) : hs.piece p = ⊥

In an effective Hodge structure, a component with negative first index vanishes.

theorem TauCeti.Hodge.HodgeStructureOn.IsEffective.piece_eq_bot_of_weight_lt {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} (h : hs.IsEffective) {p : ℤ} (hp : n < p) : hs.piece p = ⊥

In an effective Hodge structure, a component with first index above the weight vanishes.