Documentation

TauCeti.Geometry.Hodge.Mixed.Strictness

Strictness of a morphism of mixed Hodge structures #

A morphism of mixed Hodge structures is strict: an element of the target that lies in a step of a filtration and in the image of the morphism is already the image of an element of the corresponding step of the source. Filtration-preserving maps are not strict in general — this is the theorem that makes the category of mixed Hodge structures abelian — and the proof is Deligne's bigrading.

Both filtrations are recovered from the bigrading I^{p,q} (TauCeti.Hodge.MixedHodgeStructure.WC_eq_iSup_deligneSplitting and TauCeti.Hodge.MixedHodgeStructure.F_eq_iSup_deligneSplitting) as suprema of the pieces over a set of bidegrees, a morphism carries I^{p,q} into I^{p,q} (TauCeti.Hodge.MixedHodgeStructure.Hom.map_deligneSplitting_le), and the pieces of the target are independent. Strictness for both filtrations at once is then the lattice statement that in a family B ≤ A with A independent, the sum of the B over all indices meets the sum of the A over a set S of indices in exactly the sum of the B over S: an element of the intersection has no component of the target's bigrading outside S, so the source element producing it may be truncated to its own components in S.

The weight filtration is a rational datum, and its strictness is stated rationally. It descends from the complex statement because ℂ is faithfully flat over ℚ, so an inclusion of rational subspaces can be tested after complexification (TauCeti.Hodge.rationalToComplexSubmodule_le_iff); only the trivial half of the compatibility of complexification with intersections is needed.

Main declarations #

References #

Deligne, Théorie de Hodge II, 1.2.10 and 2.3.5; Peters–Steenbrink, Mixed Hodge Structures, Theorem 3.13. This is the milestone of Layer L2 of the Hodge structures roadmap.

The image of a morphism, bigraded #

source
theorem TauCeti.Hodge.MixedHodgeStructure.Hom.range_eq_iSup_map_deligneSplittingFamily {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) :
f.toLinearMap.range = ⨆ (pq : ℤ × ℤ), Submodule.map f.toLinearMap (source.deligneSplittingFamily pq)

The image of a morphism of mixed Hodge structures is the sum of the images of the bigrading pieces of its source: the bigrading of the source spans.

source
theorem TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_iSup_deligneSplittingFamily_eq_map_iSup {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) (P : ℤ × ℤ → Prop) :
f.toLinearMap.range ⊓ ⨆ (pq : ℤ × ℤ), ⨆ (_ : P pq), target.deligneSplittingFamily pq = Submodule.map f.toLinearMap (⨆ (pq : ℤ × ℤ), ⨆ (_ : P pq), source.deligneSplittingFamily pq)

Strictness against a set of bidegrees. The image of a morphism meets the sum of the target's bigrading pieces over the bidegrees satisfying P in exactly the image of the corresponding sum for the source.

Both filtrations of a mixed Hodge structure are sums of bigrading pieces over such a set, so this single statement carries every strictness assertion below.

Strictness #

source
@[simp]
theorem TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_F_eq_map_F {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) (p : ℤ) :
f.toLinearMap.range ⊓ target.F p = Submodule.map f.toLinearMap (source.F p)

Strictness of a morphism of mixed Hodge structures for the Hodge filtration. A complex vector lying both in the image of f and in the target's Hodge step F^p is the image of a vector of the source's F^p.

The two filtration steps are the sums of the bigrading pieces of first index at least p, and f respects the bigrading, so a preimage may be truncated to its components of first index at least p without changing its image.

source
@[simp]
theorem TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_WC_eq_map_WC {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) (k : ℤ) :
f.toLinearMap.range ⊓ target.WC k = Submodule.map f.toLinearMap (source.WC k)

Strictness of a morphism of mixed Hodge structures for the complexified weight filtration.

source
@[simp]
theorem TauCeti.Hodge.MixedHodgeStructure.Hom.range_inf_WQ_eq_map_WQ {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) (k : ℤ) :
f.toRatLinearMap.range ⊓ target.WQ k = Submodule.map f.toRatLinearMap (source.WQ k)

Strictness of a morphism of mixed Hodge structures for the weight filtration. A rational vector lying both in the image of f and in the target's weight step W_k is the image of a vector of the source's W_k.

The weight filtration is rational, so this is the form the milestone takes; it descends from the complex statement because complexification of rational subspaces reflects inclusions. Only the inclusion (A ∩ B)_ℂ ≤ A_ℂ ∩ B_ℂ is used, which is monotonicity.

Inverses of bijective morphisms #

source
noncomputable def TauCeti.Hodge.MixedHodgeStructure.Hom.invOfBijective {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) (hf : Function.Bijective ⇑f.toRatLinearMap) :
target.Hom source

A bijective morphism of mixed Hodge structures has an inverse morphism. The inverse of the underlying rational map preserves both filtrations: by strictness, a vector of a filtration step of the target is the image of a vector of the same step of the source.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.Hom.invOfBijective_toRatLinearMap {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) (hf : Function.Bijective ⇑f.toRatLinearMap) :
    (f.invOfBijective hf).toRatLinearMap = ↑(LinearEquiv.ofBijective f.toRatLinearMap hf).symm

    The rational map underlying the inverse of a bijective morphism is the inverse linear map.

    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.Hom.invOfBijective_comp {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) (hf : Function.Bijective ⇑f.toRatLinearMap) :
    (f.invOfBijective hf).comp f = id source

    The inverse of a bijective morphism is a left inverse.

    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.Hom.comp_invOfBijective {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) (hf : Function.Bijective ⇑f.toRatLinearMap) :
    f.comp (f.invOfBijective hf) = id target

    The inverse of a bijective morphism is a right inverse.