Documentation

TauCeti.Geometry.Hodge.Mixed.Substructure

Sub-mixed Hodge structures #

A rational subspace of the ambient space of a mixed Hodge structure is a sub-mixed Hodge structure when its complexification is spanned by its intersections with the pieces I^{p,q} of Deligne's bigrading. This is the mixed counterpart of the condition defining TauCeti.Hodge.HodgeStructureOn.IsSubstructure in the pure theory, where the Hodge components take the place of the bigrading pieces; conjugation stability, a separate requirement there, is automatic here because the subspace is rational.

The condition is what makes the intersection filtrations behave: since both filtrations of a mixed Hodge structure are suprema of bigrading pieces over a set of bidegrees, intersecting either of them with such a subspace gives the supremum of the corresponding pieces of the subspace (TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.WC_inf_eq_iSup_inf_deligneSplitting and …F_inf_eq_iSup_inf_deligneSplitting).

Sums and intersections of sub-mixed Hodge structures are again such. Examples are recorded: the zero subspace and the whole space, the steps of the weight filtration, and — this is the point — the kernel and the image of a morphism. For the kernel the argument is that the complexified kernel is the kernel of the complexified map (TauCeti.Hodge.MixedHodgeStructure.Hom.ker_toLinearMap), that the bigrading of the source spans and that of the target is independent, so a vector killed by the map has each of its bigraded parts killed as well. For the image it is that the image is the sum of the images of the bigrading pieces, each of which already sits in the piece of the same bidegree.

Being a sub-mixed Hodge structure is a condition on the subspace alone. Promoting such a subspace to a TauCeti.Hodge.MixedHodgeStructure in its own right needs more than the condition: that structure carries base-change models for the subspace alongside the induced filtrations.

Main declarations #

References #

Deligne, Théorie de Hodge II, 1.2.10 and 2.3.5; Peters–Steenbrink, Mixed Hodge Structures, Ch. 3, where the bigrading criterion is how subobjects of the mixed theory are recognised.

source
structure TauCeti.Hodge.MixedHodgeStructure.IsSubstructure {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ℂ) (U : Submodule ℚ Vℚ) :
Prop

A sub-mixed Hodge structure of mhs: a rational subspace whose complexification is spanned by its intersections with the pieces of Deligne's bigrading.

The reverse inequality holds for any rational subspace, so the single field is the whole of the spanning condition; see TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.eq_iSup_inf_deligneSplittingFamily.

Instances For
    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.eq_iSup_inf_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ℂ} {U : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) :
    rationalToComplexSubmodule hℚ hℂ U = ⨆ (pq : ℤ × ℤ), rationalToComplexSubmodule hℚ hℂ U ⊓ mhs.deligneSplittingFamily pq

    The complexification of a sub-mixed Hodge structure is the sum of its intersections with the pieces of Deligne's bigrading.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.iSup₂_deligneSplittingFamily_inf {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ℂ} {U : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) (P : ℤ × ℤ → Prop) :
    (⨆ (pq : ℤ × ℤ), ⨆ (_ : P pq), mhs.deligneSplittingFamily pq) ⊓ rationalToComplexSubmodule hℚ hℂ U = ⨆ (pq : ℤ × ℤ), ⨆ (_ : P pq), rationalToComplexSubmodule hℚ hℂ U ⊓ mhs.deligneSplittingFamily pq

    A sum of bigrading pieces traces on a sub-mixed Hodge structure in the corresponding sum of their traces. Both filtrations of a mixed Hodge structure are such sums, so this carries the two statements below.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.WC_inf_eq_iSup_inf_deligneSplitting {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ℂ} {U : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) (k : ℤ) :
    mhs.WC k ⊓ rationalToComplexSubmodule hℚ hℂ U = ⨆ (pq : ℤ × ℤ), ⨆ (_ : pq.1 + pq.2 ≤ k), rationalToComplexSubmodule hℚ hℂ U ⊓ mhs.deligneSplitting pq.1 pq.2

    The weight filtration traced on a sub-mixed Hodge structure is bigraded: its k-th step is the sum of the traces of the bigrading pieces of total degree at most k.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.F_inf_eq_iSup_inf_deligneSplitting {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ℂ} {U : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) (p : ℤ) :
    mhs.F p ⊓ rationalToComplexSubmodule hℚ hℂ U = ⨆ (pq : ℤ × ℤ), ⨆ (_ : p ≤ pq.1), rationalToComplexSubmodule hℚ hℂ U ⊓ mhs.deligneSplitting pq.1 pq.2

    The Hodge filtration traced on a sub-mixed Hodge structure is bigraded: its p-th step is the sum of the traces of the bigrading pieces of first index at least p.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.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 ℂ ιℂ} {mhs : MixedHodgeStructure hℚ hℂ} {U U' : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) (h' : mhs.IsSubstructure U') :
    mhs.IsSubstructure (U ⊔ U')

    Sub-mixed Hodge structures are closed under sums.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inf {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ℂ} {U U' : Submodule ℚ Vℚ} (h : mhs.IsSubstructure U) (h' : mhs.IsSubstructure U') :
    mhs.IsSubstructure (U ⊓ U')

    Sub-mixed Hodge structures are closed under intersections.

    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.isSubstructure_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 ℂ ιℂ} {mhs : MixedHodgeStructure hℚ hℂ} :
    mhs.IsSubstructure ⊥

    The zero subspace is a sub-mixed Hodge structure.

    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.isSubstructure_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 ℂ ιℂ} {mhs : MixedHodgeStructure hℚ hℂ} :
    mhs.IsSubstructure ⊤

    The whole space is a sub-mixed Hodge structure: Deligne's bigrading spans.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.isSubstructure_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 ℂ ιℂ} {mhs : MixedHodgeStructure hℚ hℂ} (k : ℤ) :
    mhs.IsSubstructure (mhs.WQ k)

    Every step of the weight filtration is a sub-mixed Hodge structure: it is the sum of the bigrading pieces of total degree at most k, each of which it contains.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.Hom.isSubstructure_ker {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} {V'ℤ : Type u'} {V'ℚ : Type v'} {V'ℂ : Type w'} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℚ : IsBaseChange ℚ ι'ℚ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {source : MixedHodgeStructure hℚ hℂ} {target : MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom target) :
    source.IsSubstructure f.toRatLinearMap.ker

    The kernel of a morphism of mixed Hodge structures is a sub-mixed Hodge structure.

    source
    theorem TauCeti.Hodge.MixedHodgeStructure.Hom.isSubstructure_range {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} {V'ℤ : Type u'} {V'ℚ : Type v'} {V'ℂ : Type w'} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℤ] [AddCommGroup V'ℚ] [Module ℚ V'ℚ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {ι'ℚ : V'ℤ →ₗ[ℤ] V'ℚ} {ι'ℂ : V'ℤ →ₗ[ℤ] V'ℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℚ : IsBaseChange ℚ ι'ℚ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {source : MixedHodgeStructure hℚ hℂ} {target : MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom target) :
    target.IsSubstructure f.toRatLinearMap.range

    The image of a morphism of mixed Hodge structures is a sub-mixed Hodge structure.