Quotients of mixed Hodge structures #
A sub-mixed Hodge structure determines a mixed Hodge structure on the quotient. Its integral, rational, and complex carriers are the corresponding quotients; its weight and Hodge filtrations are the images of the ambient filtrations. Deligne's bigrading descends componentwise, so the quotient is again a mixed Hodge structure and the quotient map is a morphism.
This is the object-level quotient construction needed to form cokernels in the category of mixed Hodge structures. It complements the induced structure on a rational subspace: kernels use that subobject construction, while cokernels use the quotient by the range.
Main declarations #
TauCeti.Hodge.IsHodgeBigrading.map_mkQ: a Hodge bigrading descends through a subspace spanned by its intersections with the bigrading pieces.TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient: the induced mixed Hodge structure on the quotient by a sub-mixed Hodge structure.TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.projection: the quotient projection as a morphism of mixed Hodge structures.TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.lift: the universal factorization of a morphism annihilating the substructure through the quotient projection.
References #
Deligne, Théorie de Hodge II, §2.3; Peters–Steenbrink, Mixed Hodge Structures, Chapter 3.
theorem
TauCeti.Hodge.IsHodgeBigrading.map_mkQ
{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.map U.mkQ (WQ k))
(fun (p : ℤ) => Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (F p)) fun (pq : ℤ × ℤ) =>
Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (I pq)
Descending a Hodge bigrading to a quotient. If a rational subspace is spanned by its intersections with the bigrading pieces, then the images of those pieces form a Hodge bigrading for the image filtrations on the quotient.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient
{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)
:
The mixed Hodge structure induced on the quotient by a sub-mixed Hodge structure. Both filtrations and every bigrading piece are the images of their ambient counterparts.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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 : ℤ)
:
The rational weight filtration on the quotient is the image of the ambient weight filtration.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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 : ℤ)
:
The Hodge filtration on the quotient is the image of the ambient Hodge filtration.
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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 : ℤ)
:
The complex weight filtration on the quotient is the image of the ambient complex weight filtration.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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 : ℤ)
:
The conjugate Hodge filtration on the quotient is the image of the ambient conjugate Hodge filtration.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.projection
{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)
:
The quotient projection is a morphism of mixed Hodge structures.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.projection_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)
:
The rational map underlying the quotient projection is the canonical quotient map.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.projection_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)
:
On complex vectors, the quotient projection is the canonical complex quotient map.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.lift
{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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
(f : mhs.Hom target)
(hf : U ≤ f.toRatLinearMap.ker)
:
A morphism annihilating a sub-mixed Hodge structure factors through its quotient.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.lift_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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
(f : mhs.Hom target)
(hf : U ≤ f.toRatLinearMap.ker)
:
The rational map underlying the quotient lift is the usual linear quotient lift.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.lift_comp_projection
{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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
(f : mhs.Hom target)
(hf : U ≤ f.toRatLinearMap.ker)
:
The quotient lift restricts along the quotient projection to the original morphism.
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotientHom_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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
{f g : hU.quotient.Hom target}
(hfg : f.comp hU.projection = g.comp hU.projection)
:
Morphisms out of the quotient are equal when they agree after the quotient projection.
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotientHom_ext_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 ℂ ιℂ}
{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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
{f g : hU.quotient.Hom target}
:
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.eq_lift
{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 ℂ ι'ℂ}
{target : MixedHodgeStructure h'ℚ h'ℂ}
{f : mhs.Hom target}
{hf : U ≤ f.toRatLinearMap.ker}
{g : hU.quotient.Hom target}
(hg : g.comp hU.projection = f)
:
The quotient lift is the unique morphism whose composite with the projection is f.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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.quotient.deligneSplittingFamily = fun (pq : ℤ × ℤ) =>
Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (mhs.deligneSplittingFamily pq)
The Deligne bigrading of the quotient is the image of the ambient Deligne bigrading.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.IsSubstructure.quotient_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.quotient.deligneSplitting p q = Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (mhs.deligneSplitting p q)
A Deligne bigrading piece of the quotient is the image of the corresponding ambient piece.