Graded pieces of a rational weight filtration

A mixed Hodge structure carries an increasing weight filtration W on the rational model Vℚ and a decreasing Hodge filtration F on the complex model Vℂ, and asks that F induce a pure Hodge structure of weight k on each graded piece grᵂ_k = W_k / W_{k-1}. This file supplies the objects that condition is stated against.

The graded piece is taken rationally, and the pure structure lives on its complexification ℂ ⊗[ℚ] grᵂ_k. That model is preferred to the complex graded piece (W_k)_ℂ / (W_{k-1})_ℂ because it carries a canonical conjugation for free: ℂ ⊗[ℚ] U is a base change of the ℚ-vector space U along ℤ → ℂ (TauCeti.isBaseChange_ratTensorMap), so TauCeti.Hodge.latticeConj applies to it verbatim. The two models are identified by TauCeti.Hodge.gradedComplexEquiv, which says that complexification commutes with the graded quotient, and the Hodge filtration is transported across that identification.

Main declarations

• TauCeti.Hodge.weightGradedRat, TauCeti.Hodge.weightGradedComplex: the rational and complex graded pieces of a filtration.
• TauCeti.Hodge.gradedComplexEquiv: complexification commutes with the weight-graded quotient.
• TauCeti.Hodge.weightGradedRatMap, TauCeti.Hodge.weightGradedComplexMap: the maps induced on the graded pieces by a linear map preserving every step of the filtration, together with their functoriality and the naturality of TauCeti.Hodge.gradedComplexEquiv in that map.
• TauCeti.Hodge.complexGradedF, TauCeti.Hodge.gradedF: the Hodge filtration induced on the complex graded piece and on the complexified rational graded piece.
• TauCeti.Hodge.complexGradedConjugation, TauCeti.Hodge.gradedComplexConjugation: the conjugation induced on a complex graded piece by a conjugation stabilising the two filtration steps it is built from, and its instance for a complexified rational filtration and lattice conjugation.
• TauCeti.Hodge.gradedComplexEquiv_latticeConj: the comparison of the two graded models intertwines those conjugations.
• TauCeti.Hodge.gradedEquivOfEqBotOfEqTop: across a step where the weight filtration jumps from zero to everything, the complexified graded piece is the whole complex model, compatibly with the conjugations and with the induced filtration.

The conventions for opposed and induced filtrations follow Deligne, Théorie de Hodge II, §1.2.1; the graded-piece comparison is the one used throughout Peters–Steenbrink, Mixed Hodge Structures, Ch. 3. The signatures of weightGradedRat, gradedComplexEquiv and gradedF are adapted from the proposed definitions in HodgeStructures/Suggested.lean, whose definitive mathematical specification is the accompanying Hodge structures roadmap.

theorem TauCeti.Hodge.map_range_lTensor_submoduleOf {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 ℂ ιℂ) {A B : Submodule ℚ Vℚ} (hAB : A ≤ B) : Submodule.map (↑(rationalToComplexSubmoduleEquiv hℚ hℂ B)) ((TensorProduct.AlgebraTensorModule.lTensor ℂ ℂ) (↑ℚ (A.submoduleOf B).subtype)).range = (rationalToComplexSubmodule hℚ hℂ A).submoduleOf (rationalToComplexSubmodule hℚ hℂ B)

Complexifying the inclusion of one rational subspace into a larger one, then identifying the larger tensor product with the complexified subspace, has the complexification of the smaller subspace as its range.

@[reducible, inline]

abbrev TauCeti.Hodge.weightGradedRat {Vℚ : Type v} [AddCommGroup Vℚ] [Module ℚ Vℚ] (WQ : ℤ → Submodule ℚ Vℚ) (k : ℤ) : Type v

The k-th graded piece grᵂ_k = W_k / W_{k-1} of an increasing rational filtration W. The lower step is viewed inside W_k through Submodule.submoduleOf.

@[reducible, inline]

abbrev TauCeti.Hodge.weightGradedComplex {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (k : ℤ) : Type w

The k-th graded piece of an increasing complex filtration.

@[simp]

theorem TauCeti.Hodge.weightGradedComplex_mk_eq_mk_iff {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (k : ℤ) (x y : ↥(WC k)) : Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ ↑x - ↑y ∈ WC (k - 1)

Two classes in the k-th complex graded piece agree exactly when their representatives differ by a vector of the step below.

theorem TauCeti.Hodge.weightGradedComplex_mk_eq_zero_iff {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (k : ℤ) (x : ↥(WC k)) : Submodule.Quotient.mk x = 0 ↔ ↑x ∈ WC (k - 1)

A class in the k-th complex graded piece vanishes exactly when its representative already lies in the step below.

This is not a simp lemma: Submodule.Quotient.mk_eq_zero already simplifies its left-hand side, so the simpNF linter rejects the attribute here.

noncomputable def TauCeti.Hodge.gradedComplexEquiv {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ℚ) (hWQ : Monotone WQ) (k : ℤ) : TensorProduct ℚ ℂ (weightGradedRat WQ k) ≃ₗ[ℂ] weightGradedComplex (fun (k : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ k)) k

Complexification commutes with the weight-graded quotient: the complexification of the rational graded piece grᵂ_k is the graded piece of the complexified filtration.

@[simp]

theorem TauCeti.Hodge.gradedComplexEquiv_tmul_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 ℂ ιℂ) (WQ : ℤ → Submodule ℚ Vℚ) (hWQ : Monotone WQ) (k : ℤ) (z : ℂ) (x : ↥(WQ k)) : (gradedComplexEquiv hℚ hℂ WQ hWQ k) (z ⊗ₜ[ℚ] Submodule.Quotient.mk x) = Submodule.Quotient.mk ((rationalToComplexSubmoduleEquiv hℚ hℂ (WQ k)) (z ⊗ₜ[ℚ] x))

noncomputable def TauCeti.Hodge.weightGradedRatMap {Vℚ : Type v} [AddCommGroup Vℚ] [Module ℚ Vℚ] {V'ℚ : Type v'} [AddCommGroup V'ℚ] [Module ℚ V'ℚ] (WQ : ℤ → Submodule ℚ Vℚ) (W'Q : ℤ → Submodule ℚ V'ℚ) (f : Vℚ →ₗ[ℚ] V'ℚ) (hf : ∀ (k : ℤ), ∀ x ∈ WQ k, f x ∈ W'Q k) (k : ℤ) : weightGradedRat WQ k →ₗ[ℚ] weightGradedRat W'Q k

The map induced on the k-th rational graded piece by a linear map carrying every step of one increasing filtration into the corresponding step of another.

@[simp]

theorem TauCeti.Hodge.weightGradedRatMap_mk {Vℚ : Type v} [AddCommGroup Vℚ] [Module ℚ Vℚ] {V'ℚ : Type v'} [AddCommGroup V'ℚ] [Module ℚ V'ℚ] (WQ : ℤ → Submodule ℚ Vℚ) (W'Q : ℤ → Submodule ℚ V'ℚ) (f : Vℚ →ₗ[ℚ] V'ℚ) (hf : ∀ (k : ℤ), ∀ x ∈ WQ k, f x ∈ W'Q k) (k : ℤ) (x : ↥(WQ k)) : (weightGradedRatMap WQ W'Q f hf k) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨f ↑x, ⋯⟩

The induced map on a rational graded piece sends the class of a vector to the class of its image.

noncomputable def TauCeti.Hodge.weightGradedComplexMap {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] {V'ℂ : Type w'} [AddCommGroup V'ℂ] [Module ℂ V'ℂ] (WC : ℤ → Submodule ℂ Vℂ) (W'C : ℤ → Submodule ℂ V'ℂ) (g : Vℂ →ₗ[ℂ] V'ℂ) (hg : ∀ (k : ℤ), ∀ x ∈ WC k, g x ∈ W'C k) (k : ℤ) : weightGradedComplex WC k →ₗ[ℂ] weightGradedComplex W'C k

The map induced on the k-th graded piece of a complex filtration by a complex-linear map carrying every step into the corresponding step of another filtration.

@[simp]

theorem TauCeti.Hodge.weightGradedComplexMap_mk {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] {V'ℂ : Type w'} [AddCommGroup V'ℂ] [Module ℂ V'ℂ] (WC : ℤ → Submodule ℂ Vℂ) (W'C : ℤ → Submodule ℂ V'ℂ) (g : Vℂ →ₗ[ℂ] V'ℂ) (hg : ∀ (k : ℤ), ∀ x ∈ WC k, g x ∈ W'C k) (k : ℤ) (x : ↥(WC k)) : (weightGradedComplexMap WC W'C g hg k) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨g ↑x, ⋯⟩

The induced map on a complex graded piece sends the class of a vector to the class of its image.

@[simp]

theorem TauCeti.Hodge.weightGradedComplexMap_id {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (k : ℤ) : weightGradedComplexMap WC WC LinearMap.id ⋯ k = LinearMap.id

Passage to the complex graded pieces sends the identity map to the identity.

@[simp]

theorem TauCeti.Hodge.weightGradedComplexMap_comp {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] {V'ℂ : Type w'} [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {V''ℂ : Type u_1} [AddCommGroup V''ℂ] [Module ℂ V''ℂ] (WC : ℤ → Submodule ℂ Vℂ) (W'C : ℤ → Submodule ℂ V'ℂ) (W''C : ℤ → Submodule ℂ V''ℂ) (f : Vℂ →ₗ[ℂ] V'ℂ) (hf : ∀ (k : ℤ), ∀ x ∈ WC k, f x ∈ W'C k) (g : V'ℂ →ₗ[ℂ] V''ℂ) (hg : ∀ (k : ℤ), ∀ x ∈ W'C k, g x ∈ W''C k) (k : ℤ) : weightGradedComplexMap WC W''C (g ∘ₗ f) ⋯ k = weightGradedComplexMap W'C W''C g hg k ∘ₗ weightGradedComplexMap WC W'C f hf k

Passage to the complex graded pieces is compatible with composition.

@[simp]

theorem TauCeti.Hodge.weightGradedRatMap_id {Vℚ : Type v} [AddCommGroup Vℚ] [Module ℚ Vℚ] (WQ : ℤ → Submodule ℚ Vℚ) (k : ℤ) : weightGradedRatMap WQ WQ LinearMap.id ⋯ k = LinearMap.id

Passage to the rational graded pieces sends the identity map to the identity.

@[simp]

theorem TauCeti.Hodge.weightGradedRatMap_comp {Vℚ : Type v} [AddCommGroup Vℚ] [Module ℚ Vℚ] {V'ℚ : Type v'} [AddCommGroup V'ℚ] [Module ℚ V'ℚ] {V''ℚ : Type u_1} [AddCommGroup V''ℚ] [Module ℚ V''ℚ] (WQ : ℤ → Submodule ℚ Vℚ) (W'Q : ℤ → Submodule ℚ V'ℚ) (W''Q : ℤ → Submodule ℚ V''ℚ) (f : Vℚ →ₗ[ℚ] V'ℚ) (hf : ∀ (k : ℤ), ∀ x ∈ WQ k, f x ∈ W'Q k) (g : V'ℚ →ₗ[ℚ] V''ℚ) (hg : ∀ (k : ℤ), ∀ x ∈ W'Q k, g x ∈ W''Q k) (k : ℤ) : weightGradedRatMap WQ W''Q (g ∘ₗ f) ⋯ k = weightGradedRatMap W'Q W''Q g hg k ∘ₗ weightGradedRatMap WQ W'Q f hf k

Passage to the rational graded pieces is compatible with composition.

theorem TauCeti.Hodge.gradedComplexEquiv_baseChange_weightGradedRatMap {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'} {V'ℚ : Type v'} {V'ℂ : Type w'} [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (h'ℚ : IsBaseChange ℚ ι'ℚ) (h'ℂ : IsBaseChange ℂ ι'ℂ) (WQ : ℤ → Submodule ℚ Vℚ) (hWQ : Monotone WQ) (W'Q : ℤ → Submodule ℚ V'ℚ) (hW'Q : Monotone W'Q) (f : Vℚ →ₗ[ℚ] V'ℚ) (hf : ∀ (k : ℤ), ∀ x ∈ WQ k, f x ∈ W'Q k) (k : ℤ) (t : TensorProduct ℚ ℂ (weightGradedRat WQ k)) : (gradedComplexEquiv h'ℚ h'ℂ W'Q hW'Q k) ((LinearMap.baseChange ℂ (weightGradedRatMap WQ W'Q f hf k)) t) = (weightGradedComplexMap (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ j)) (fun (j : ℤ) => rationalToComplexSubmodule h'ℚ h'ℂ (W'Q j)) (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ f) ⋯ k) ((gradedComplexEquiv hℚ hℂ WQ hWQ k) t)

The comparison TauCeti.Hodge.gradedComplexEquiv is natural in the filtered map: the square formed by the map induced on the rational graded pieces, its base change, and the map induced by the complexification on the graded pieces of the complexified filtrations, commutes. Preservation of the complexified filtration is not a separate hypothesis: it follows from the rational one by TauCeti.Hodge.map_rationalToComplexSubmodule_le.

noncomputable def TauCeti.Hodge.complexGradedF {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC F : ℤ → Submodule ℂ Vℂ) (k p : ℤ) : Submodule ℂ (weightGradedComplex WC k)

The Hodge filtration induced on the k-th complex graded piece: the image of F^p ∩ W_k under the quotient map W_k → W_k / W_{k-1}.

noncomputable def TauCeti.Hodge.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ℚ) (hWQ : Monotone WQ) (F : ℤ → Submodule ℂ Vℂ) (k p : ℤ) : Submodule ℂ (TensorProduct ℚ ℂ (weightGradedRat WQ k))

The Hodge filtration induced on the complexification of the rational graded piece grᵂ_k, transported from the complex graded piece along gradedComplexEquiv.

@[simp]

theorem TauCeti.Hodge.mem_complexGradedF_iff {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC F : ℤ → Submodule ℂ Vℂ) (k p : ℤ) (x : weightGradedComplex WC k) : x ∈ complexGradedF WC F k p ↔ ∃ (y : ↥(WC k)), ↑y ∈ F p ∧ Submodule.Quotient.mk y = x

Membership in the induced filtration on a complex graded piece is witnessed by a representative in the corresponding ambient Hodge-filtration step.

@[simp]

theorem TauCeti.Hodge.mem_gradedF_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ℚ) (hWQ : Monotone WQ) (F : ℤ → Submodule ℂ Vℂ) (k p : ℤ) (x : TensorProduct ℚ ℂ (weightGradedRat WQ k)) : x ∈ gradedF hℚ hℂ WQ hWQ F k p ↔ ∃ (y : ↥(rationalToComplexSubmodule hℚ hℂ (WQ k))), ↑y ∈ F p ∧ Submodule.Quotient.mk y = (gradedComplexEquiv hℚ hℂ WQ hWQ k) x

Membership in the filtration on a complexified rational graded piece is detected after transport to the complex graded piece and represented there by an element of F p.

theorem TauCeti.Hodge.complexGradedF_antitone {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC F : ℤ → Submodule ℂ Vℂ) (hF : Antitone F) (k : ℤ) : Antitone (complexGradedF WC F k)

The induced filtration on a complex graded piece is decreasing.

@[simp]

theorem TauCeti.Hodge.complexGradedF_of_eq_top {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC F : ℤ → Submodule ℂ Vℂ) {k p : ℤ} (hp : F p = ⊤) : complexGradedF WC F k p = ⊤

A step where the Hodge filtration is everything induces everything on a graded piece.

@[simp]

theorem TauCeti.Hodge.complexGradedF_of_eq_bot {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC F : ℤ → Submodule ℂ Vℂ) {k p : ℤ} (hp : F p = ⊥) : complexGradedF WC F k p = ⊥

A step where the Hodge filtration is zero induces zero on a graded piece.

theorem TauCeti.Hodge.gradedF_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ℚ) (hWQ : Monotone WQ) (F : ℤ → Submodule ℂ Vℂ) (hF : Antitone F) (k : ℤ) : Antitone (gradedF hℚ hℂ WQ hWQ F k)

The filtration induced on a complexified rational graded piece is decreasing.

@[simp]

theorem TauCeti.Hodge.gradedF_of_eq_top {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ℚ) (hWQ : Monotone WQ) (F : ℤ → Submodule ℂ Vℂ) {k p : ℤ} (hp : F p = ⊤) : gradedF hℚ hℂ WQ hWQ F k p = ⊤

A step where the Hodge filtration is everything induces everything on a graded piece.

@[simp]

theorem TauCeti.Hodge.gradedF_of_eq_bot {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ℚ) (hWQ : Monotone WQ) (F : ℤ → Submodule ℂ Vℂ) {k p : ℤ} (hp : F p = ⊥) : gradedF hℚ hℂ WQ hWQ F k p = ⊥

A step where the Hodge filtration is zero induces zero on a graded piece.

noncomputable def TauCeti.Hodge.complexGradedConjugation {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (ω : Conjugation Vℂ) (k : ℤ) (hk : ∀ x ∈ WC k, ω.toEquiv x ∈ WC k) (hk₁ : ∀ x ∈ WC (k - 1), ω.toEquiv x ∈ WC (k - 1)) : Conjugation (weightGradedComplex WC k)

The conjugation induced on the k-th complex graded piece by a conjugation of the ambient space that stabilises the two steps WC k and WC (k - 1) the piece is built from.

@[simp]

theorem TauCeti.Hodge.complexGradedConjugation_mk {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (ω : Conjugation Vℂ) (k : ℤ) (hk : ∀ x ∈ WC k, ω.toEquiv x ∈ WC k) (hk₁ : ∀ x ∈ WC (k - 1), ω.toEquiv x ∈ WC (k - 1)) (x : ↥(WC k)) : (complexGradedConjugation WC ω k hk hk₁).toEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨ω.toEquiv ↑x, ⋯⟩

The induced conjugation on a complex graded piece acts on classes through the ambient conjugation.

theorem TauCeti.Hodge.map_complexGradedConjugation_complexGradedF {Vℂ : Type w} [AddCommGroup Vℂ] [Module ℂ Vℂ] (WC : ℤ → Submodule ℂ Vℂ) (ω : Conjugation Vℂ) (k : ℤ) (hk : ∀ x ∈ WC k, ω.toEquiv x ∈ WC k) (hk₁ : ∀ x ∈ WC (k - 1), ω.toEquiv x ∈ WC (k - 1)) (F : ℤ → Submodule ℂ Vℂ) (p : ℤ) : Submodule.map (↑(complexGradedConjugation WC ω k hk hk₁).toEquiv) (complexGradedF WC F k p) = complexGradedF WC (fun (q : ℤ) => Submodule.map (↑ω.toEquiv) (F q)) k p

Conjugating the filtration induced on a complex graded piece is inducing the conjugate filtration.

noncomputable def TauCeti.Hodge.gradedComplexConjugation {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ℚ) (k : ℤ) : Conjugation (weightGradedComplex (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ j)) k)

The conjugation induced on the k-th graded piece of a complexified rational weight filtration by lattice conjugation. Every step of the filtration is the complexification of a rational subspace, hence conjugation-stable.

@[simp]

theorem TauCeti.Hodge.gradedComplexConjugation_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 ℂ ιℂ) (WQ : ℤ → Submodule ℚ Vℚ) (k : ℤ) (x : ↥(rationalToComplexSubmodule hℚ hℂ (WQ k))) : (gradedComplexConjugation hℚ hℂ WQ k).toEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨(latticeConj hℂ) ↑x, ⋯⟩

The induced conjugation on the graded piece of a complexified rational filtration acts on a class through lattice conjugation of a representative.

theorem TauCeti.Hodge.map_gradedComplexConjugation_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ℂ) (k p : ℤ) : Submodule.map (↑(gradedComplexConjugation hℚ hℂ WQ k).toEquiv) (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 p

Conjugating the filtration induced on the graded piece of a complexified rational filtration is inducing the conjugate filtration.

theorem TauCeti.Hodge.gradedComplexEquiv_latticeConj {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ℚ) (hWQ : Monotone WQ) (k : ℤ) (x : TensorProduct ℚ ℂ (weightGradedRat WQ k)) : (gradedComplexEquiv hℚ hℂ WQ hWQ k) ((latticeConj ⋯) x) = (gradedComplexConjugation hℚ hℂ WQ k).toEquiv ((gradedComplexEquiv hℚ hℂ WQ hWQ k) x)

The comparison TauCeti.Hodge.gradedComplexEquiv intertwines the conjugations: the canonical conjugation of the complexified rational graded piece corresponds to the conjugation that lattice conjugation induces on the complex graded piece.

This is what makes the pure Hodge structure carried by ℂ ⊗[ℚ] grᵂ_k transportable to the complex graded piece (W_k)_ℂ / (W_{k-1})_ℂ, where the Hodge filtration of a mixed Hodge structure lives.

theorem TauCeti.Hodge.gradedComplexEquiv_symm_latticeConj {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ℚ) (hWQ : Monotone WQ) (k : ℤ) (y : weightGradedComplex (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (WQ j)) k) : (gradedComplexEquiv hℚ hℂ WQ hWQ k).symm ((gradedComplexConjugation hℚ hℂ WQ k).toEquiv y) = (latticeConjugation ⋯).toEquiv ((gradedComplexEquiv hℚ hℂ WQ hWQ k).symm y)

The inverse of the comparison intertwines the conjugations, in the form in which transport of a pure Hodge structure onto the complex graded piece consumes it.

noncomputable def TauCeti.Hodge.gradedEquivOfEqBotOfEqTop {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ℚ) (hWQ : Monotone WQ) {k : ℤ} (hbot : WQ (k - 1) = ⊥) (htop : WQ k = ⊤) : TensorProduct ℚ ℂ (weightGradedRat WQ k) ≃ₗ[ℂ] Vℂ

Across a step where the weight filtration jumps from zero to everything, the complexification of the rational graded piece grᵂ_k is the whole complex model.

@[simp]

theorem TauCeti.Hodge.gradedEquivOfEqBotOfEqTop_tmul_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 ℂ ιℂ) (WQ : ℤ → Submodule ℚ Vℚ) (hWQ : Monotone WQ) {k : ℤ} (hbot : WQ (k - 1) = ⊥) (htop : WQ k = ⊤) (z : ℂ) (x : ↥(WQ k)) : (gradedEquivOfEqBotOfEqTop hℚ hℂ WQ hWQ hbot htop) (z ⊗ₜ[ℚ] Submodule.Quotient.mk x) = (rationalToComplexLinearEquiv hℚ hℂ) (z ⊗ₜ[ℚ] ↑x)

theorem TauCeti.Hodge.gradedF_eq_comap {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ℚ) (hWQ : Monotone WQ) {k : ℤ} (hbot : WQ (k - 1) = ⊥) (htop : WQ k = ⊤) (F : ℤ → Submodule ℂ Vℂ) (p : ℤ) : gradedF hℚ hℂ WQ hWQ F k p = Submodule.comap (↑(gradedEquivOfEqBotOfEqTop hℚ hℂ WQ hWQ hbot htop)) (F p)

Across such a step, the filtration induced on the graded piece is the Hodge filtration itself, read through the identification above.

theorem TauCeti.Hodge.gradedEquivOfEqBotOfEqTop_latticeConj {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ℚ) (hWQ : Monotone WQ) {k : ℤ} (hbot : WQ (k - 1) = ⊥) (htop : WQ k = ⊤) (x : TensorProduct ℚ ℂ (weightGradedRat WQ k)) : (gradedEquivOfEqBotOfEqTop hℚ hℂ WQ hWQ hbot htop) ((latticeConj ⋯) x) = (latticeConj hℂ) ((gradedEquivOfEqBotOfEqTop hℚ hℂ WQ hWQ hbot htop) x)

The identification of the graded piece with the whole complex model intertwines the canonical conjugation of the complexified rational graded piece with lattice conjugation.