Mixed Hodge structures induced on rational subspaces

A rational subspace of a mixed Hodge structure which is spanned by its intersections with Deligne's bigrading inherits a mixed Hodge structure. Its integral carrier consists of the integral vectors lying in the subspace, while its complex carrier is the complexification of the rational subspace. Both filtrations and every bigrading piece are obtained by intersection with the corresponding ambient subspace in the construction.

This construction turns the subspace criterion TauCeti.Hodge.MixedHodgeStructure.IsSubstructure into an actual object. In particular, since the rational kernel and range of every mixed Hodge morphism satisfy that criterion, they can now be equipped with their induced mixed Hodge structures. This is the object-level construction needed for categorical kernels and images.

Main declarations

• TauCeti.Hodge.IsHodgeBigrading.comap_subtype: a Hodge bigrading restricts to a rational subspace spanned by its intersections with the pieces.
• TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure: the mixed Hodge structure induced on a rational subspace.
• TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusion: the inclusion of the induced structure into the ambient mixed Hodge structure.
• TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.codRestrict: the universal factorization of a morphism with values in the subspace through the inclusion.
• TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_deligneSplitting: the Deligne bigrading of the induced structure is the intersection with the ambient one.

References

Deligne, Théorie de Hodge II, §2.3; Peters–Steenbrink, Mixed Hodge Structures, Chapter 3.

theorem TauCeti.Hodge.IsHodgeBigrading.comap_subtype {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) {U : Submodule ℚ Vℚ} (hU : rationalToComplexSubmodule hℚ hℂ U ≤ ⨆ (pq : ℤ × ℤ), rationalToComplexSubmodule hℚ hℂ U ⊓ I pq) : IsHodgeBigrading ⋯ ⋯ (fun (k : ℤ) => Submodule.comap U.subtype (WQ k)) (fun (p : ℤ) => Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (F p)) fun (pq : ℤ × ℤ) => Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (I pq)

Restricting a Hodge bigrading to a rational subspace. If the complexification of a rational subspace U is spanned by its intersections with the pieces of a Hodge bigrading, then these intersections form a Hodge bigrading for the filtrations intersected with U.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure {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ℚ} (hU : mhs.IsSubstructure U) : MixedHodgeStructure ⋯ ⋯

A rational subspace satisfying the mixed-Hodge substructure criterion inherits a mixed Hodge structure by intersecting both filtrations with the subspace.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_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ℂ} {U : Submodule ℚ Vℚ} (hU : mhs.IsSubstructure U) (k : ℤ) : hU.hodgeStructure.WQ k = Submodule.comap U.subtype (mhs.WQ k)

The rational weight filtration of the induced mixed Hodge structure is obtained by intersection with the ambient weight filtration.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_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ℂ} {U : Submodule ℚ Vℚ} (hU : mhs.IsSubstructure U) (p : ℤ) : hU.hodgeStructure.F p = Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (mhs.F p)

The Hodge filtration of the induced mixed Hodge structure is obtained by intersection with the ambient Hodge filtration.

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_WC {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ℚ} (hU : mhs.IsSubstructure U) (k : ℤ) : hU.hodgeStructure.WC k = Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (mhs.WC k)

The complex weight filtration of the induced mixed Hodge structure is the ambient complex weight filtration intersected with the complexification of the subspace.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_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ℂ} {U : Submodule ℚ Vℚ} (hU : mhs.IsSubstructure U) (p : ℤ) : hU.hodgeStructure.conjF p = Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (mhs.conjF p)

The conjugate Hodge filtration of the induced mixed Hodge structure is the ambient conjugate Hodge filtration intersected with the complexification of the subspace.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusion {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ℚ} (hU : mhs.IsSubstructure U) : hU.hodgeStructure.Hom mhs

The inclusion of an induced mixed Hodge structure into its ambient mixed Hodge structure.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusion_toRatLinearMap {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ℚ} (hU : mhs.IsSubstructure U) : hU.inclusion.toRatLinearMap = U.subtype

The rational map underlying the inclusion of an induced mixed Hodge structure is the subtype map.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusion_toLinearMap {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ℚ} (hU : mhs.IsSubstructure U) : hU.inclusion.toLinearMap = (rationalToComplexSubmodule hℚ hℂ U).subtype

On complex vectors, the inclusion of an induced mixed Hodge structure is the subtype map.

noncomputable def TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.codRestrict {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ℚ} (hU : mhs.IsSubstructure U) {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 ℂ ι'ℂ} {source : MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom mhs) (hf : ∀ (x : V'ℚ), f.toRatLinearMap x ∈ U) : source.Hom hU.hodgeStructure

A morphism whose rational map takes values in a sub-mixed Hodge structure factors through the induced mixed Hodge structure.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.codRestrict_toRatLinearMap {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ℚ} (hU : mhs.IsSubstructure U) {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 ℂ ι'ℂ} {source : MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom mhs) (hf : ∀ (x : V'ℚ), f.toRatLinearMap x ∈ U) : (hU.codRestrict f hf).toRatLinearMap = LinearMap.codRestrict U f.toRatLinearMap hf

The rational map underlying a corestricted morphism is the corestricted rational map.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusion_comp_codRestrict {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ℚ} (hU : mhs.IsSubstructure U) {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 ℂ ι'ℂ} {source : MixedHodgeStructure h'ℚ h'ℂ} (f : source.Hom mhs) (hf : ∀ (x : V'ℚ), f.toRatLinearMap x ∈ U) : hU.inclusion.comp (hU.codRestrict f hf) = f

A corestricted morphism followed by the inclusion is the original morphism.

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.inclusionHom_ext {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ℚ} (hU : mhs.IsSubstructure U) {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 ℂ ι'ℂ} {source : MixedHodgeStructure h'ℚ h'ℂ} {f g : source.Hom hU.hodgeStructure} (hfg : hU.inclusion.comp f = hU.inclusion.comp g) : f = g

Morphisms into an induced mixed Hodge structure are equal when they agree after the inclusion.

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.eq_codRestrict {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ℚ} (hU : mhs.IsSubstructure U) {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 ℂ ι'ℂ} {source : MixedHodgeStructure h'ℚ h'ℂ} {f : source.Hom mhs} {hf : ∀ (x : V'ℚ), f.toRatLinearMap x ∈ U} {g : source.Hom hU.hodgeStructure} (hg : hU.inclusion.comp g = f) : g = hU.codRestrict f hf

The corestriction is the unique morphism whose composite with the inclusion is f.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_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ℚ} (hU : mhs.IsSubstructure U) : hU.hodgeStructure.deligneSplittingFamily = fun (pq : ℤ × ℤ) => Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (mhs.deligneSplittingFamily pq)

The Deligne bigrading of the induced mixed Hodge structure is the ambient Deligne bigrading intersected with the complexification of the subspace.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.hodgeStructure_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ℚ} (hU : mhs.IsSubstructure U) (p q : ℤ) : hU.hodgeStructure.deligneSplitting p q = Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (mhs.deligneSplitting p q)

A piece of the Deligne bigrading of the induced mixed Hodge structure is the ambient piece intersected with the complexification of the subspace.