Morphisms of mixed Hodge structures #
A morphism of mixed Hodge structures is a single rational linear map preserving the weight
filtration, whose complexification preserves the Hodge filtration. Only the rational map is
datum: the complex action is the canonical scalar extension
TauCeti.Hodge.rationalMapToComplex, so compatibility with the complexified weight filtration
and with lattice conjugation are theorems rather than axioms.
The conjugation-equivariance of the complex action is proved for an arbitrary complex
base-change model in TauCeti.Hodge.rationalMapToComplex_commutes_conj; it is what lets a
geometric instance, whose complex space is not literally a tensor product, use this morphism
calculus.
The principal construction here is the passage to the weight-graded pieces: a morphism of mixed
Hodge structures induces, for each k, a morphism of the pure weight-k Hodge structures
carried by the graded pieces grᵂ_k. This is functorial, and it is the form in which the mixed
theory feeds Deligne's bigrading and the strictness theorem.
Main declarations #
TauCeti.Hodge.MixedHodgeStructure.Hom: morphisms of mixed Hodge structures.TauCeti.Hodge.MixedHodgeStructure.Hom.id,…comp: identity and composition.TauCeti.Hodge.MixedHodgeStructure.Hom.map_WC_le: the complex action preserves the complexified weight filtration.TauCeti.Hodge.MixedHodgeStructure.Hom.map_conjF_le: the complex action preserves the conjugate Hodge filtration.TauCeti.Hodge.MixedHodgeStructure.Hom.commutes_conj: the complex action commutes with lattice conjugation.TauCeti.Hodge.MixedHodgeStructure.Hom.ker_toLinearMapand…range_toLinearMap: the kernel and the range of the complex action are the complexifications of the rational kernel and range.TauCeti.Hodge.MixedHodgeStructure.Hom.gradedMap: the induced map on the rational graded piecegrᵂ_k.TauCeti.Hodge.MixedHodgeStructure.Hom.gradedHom: that induced map as a morphism of the pure weight-kHodge structures, together with its functoriality.
References #
Deligne, Théorie de Hodge II, §2.3; Peters–Steenbrink, Mixed Hodge Structures, Ch. 3. The morphism convention — a single rational map with the complex action derived — is the one specified for Layer L2 of the Hodge structures roadmap.
structure
TauCeti.Hodge.MixedHodgeStructure.Hom
{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'ℂ)
:
Type (max v v')
A morphism of mixed Hodge structures.
Its only datum is a rational linear map, required to preserve every step of the weight filtration. The complex action is the canonical scalar extension of that map, and is required to preserve every step of the Hodge filtration.
The rational linear map underlying a morphism of mixed Hodge structures.
The underlying rational map preserves every step of the weight filtration.
- map_mem_F (p : ℤ) (x : Vℂ) : x ∈ source.F p → (rationalMapToComplex hℚ hℂ h'ℚ h'ℂ self.toRatLinearMap) x ∈ target.F p
The complexification of the underlying map preserves every Hodge filtration step.
Instances For
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.toLinearMap
{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)
:
The complex-linear map induced by a morphism of mixed Hodge structures.
Instances For
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instCoeFunForall
{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'ℂ}
:
A morphism of mixed Hodge structures acts on complex vectors through the complexification of its rational map.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.toLinearMap_def
{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)
:
The complex action of a morphism is the complexification of its rational map. This is the
bridge to the whole TauCeti.Hodge.rationalMapToComplex API.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.ext
{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 g : source.Hom target}
(h : ∀ (x : Vℚ), f.toRatLinearMap x = g.toRatLinearMap x)
:
Two morphisms of mixed Hodge structures are equal when their rational maps agree.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.ext_iff
{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 g : source.Hom target}
:
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.apply_rationalToComplexLinearEquiv_tmul
{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)
(z : ℂ)
(x : Vℚ)
:
f.toLinearMap ((rationalToComplexLinearEquiv hℚ hℂ) (z ⊗ₜ[ℚ] x)) = (rationalToComplexLinearEquiv h'ℚ h'ℂ) (z ⊗ₜ[ℚ] f.toRatLinearMap x)
A morphism acts on the image of a pure tensor through its rational map.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.commutes_conj
{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)
(x : Vℂ)
:
The complex action of a morphism of mixed Hodge structures commutes with lattice-induced conjugation.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_WQ_le
{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 : ℤ)
:
Preservation of a weight step in submodule-map form.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_F_le
{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 : ℤ)
:
Preservation of a Hodge step in submodule-map form.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_WC_le
{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 : ℤ)
:
A morphism of mixed Hodge structures preserves the complexified weight filtration.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_mem_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 : ℤ)
{x : Vℂ}
(hx : x ∈ source.WC k)
:
Elementwise form of preservation of the complexified weight filtration.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_conjF_le
{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 : ℤ)
:
A morphism of mixed Hodge structures preserves the conjugate Hodge filtration.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.map_mem_conjF
{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 : ℤ)
{x : Vℂ}
(hx : x ∈ source.conjF p)
:
Elementwise form of preservation of the conjugate Hodge filtration.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.ker_toLinearMap
{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)
:
The kernel of the complex action of a morphism of mixed Hodge structures is the complexification of the kernel of its rational map.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.range_toLinearMap
{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)
:
The range of the complex action of a morphism of mixed Hodge structures is the complexification of the range of its rational map.
Not @[simp]: it fires inside the left-hand sides of the strictness theorems
range_inf_F_eq_map_F and range_inf_WC_eq_map_WC, leaving those statements out of simp normal
form.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.id
{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ℂ)
:
source.Hom source
The identity morphism of a mixed Hodge structure.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.id_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 ℂ ιℂ}
{source : MixedHodgeStructure hℚ hℂ}
:
The identity morphism has the identity rational linear map underneath.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.id_apply
{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ℂ}
(x : Vℂ)
:
The identity morphism acts as the identity on complex vectors.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
:
source.Hom third
Composition of morphisms of mixed Hodge structures.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
:
The rational map underlying a composite is the composite of the rational maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_apply
{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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
(x : Vℂ)
:
Composition of morphisms is pointwise composition on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.id_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)
:
Left identity law for morphisms of mixed Hodge structures.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_id
{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)
:
Right identity law for morphisms of mixed Hodge structures.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_assoc
{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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
{V₄ℤ : Type u_1}
{V₄ℚ : Type u_2}
{V₄ℂ : Type u_3}
[AddCommGroup V₄ℤ]
[AddCommGroup V₄ℚ]
[Module ℚ V₄ℚ]
[AddCommGroup V₄ℂ]
[Module ℂ V₄ℂ]
{ι₄ℚ : V₄ℤ →ₗ[ℤ] V₄ℚ}
{ι₄ℂ : V₄ℤ →ₗ[ℤ] V₄ℂ}
{h₄ℚ : IsBaseChange ℚ ι₄ℚ}
{h₄ℂ : IsBaseChange ℂ ι₄ℂ}
{fourth : MixedHodgeStructure h₄ℚ h₄ℂ}
(h : third.Hom fourth)
(g : target.Hom third)
(f : source.Hom target)
:
Associativity of composition of morphisms of mixed Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instZero
{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'ℂ}
:
The zero morphism between two mixed Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instAdd
{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'ℂ}
:
Addition of morphisms of mixed Hodge structures, defined on their rational maps.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instNeg
{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'ℂ}
:
Negation of a morphism of mixed Hodge structures, defined on its rational map.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instSub
{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'ℂ}
:
Subtraction of morphisms of mixed Hodge structures, defined on their rational maps.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instSMulNat
{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'ℂ}
:
Natural-number multiples of a morphism of mixed Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instSMulInt
{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'ℂ}
:
Integer multiples of a morphism of mixed Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instSMulRat
{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'ℂ}
:
Rational multiples of a morphism of mixed Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instAddCommGroup
{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'ℂ}
:
AddCommGroup (source.Hom target)
Morphisms of mixed Hodge structures form an additive commutative group, transported along the injection sending a morphism to its underlying rational linear map.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.MixedHodgeStructure.Hom.instModuleRat
{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'ℂ}
:
Morphisms of mixed Hodge structures form a ℚ-vector space, transported along the same
injection: the datum of a morphism is a ℚ-linear map, and both filtrations are stable under
rational scalars.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.zero_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'ℂ}
:
The zero morphism has the zero rational linear map underneath.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.add_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 g : source.Hom target)
:
Addition of morphisms is addition of their underlying rational linear maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.neg_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)
:
Negation of a morphism is negation of its underlying rational linear map.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.sub_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 g : source.Hom target)
:
Subtraction of morphisms is subtraction of their underlying rational linear maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.zero_apply
{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'ℂ}
(x : Vℂ)
:
The zero morphism acts by zero on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.add_apply
{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 g : source.Hom target)
(x : Vℂ)
:
Addition of morphisms is pointwise addition on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.nsmul_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'ℂ}
(k : ℕ)
(f : source.Hom target)
:
Natural-number multiples of morphisms pass to their underlying rational linear maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.zsmul_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'ℂ}
(k : ℤ)
(f : source.Hom target)
:
Integer multiples of morphisms pass to their underlying rational linear maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.smul_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'ℂ}
(q : ℚ)
(f : source.Hom target)
:
Rational multiples of morphisms pass to their underlying rational linear maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.neg_apply
{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)
(x : Vℂ)
:
Negation of morphisms is pointwise negation on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.sub_apply
{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 g : source.Hom target)
(x : Vℂ)
:
Subtraction of morphisms is pointwise subtraction on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.nsmul_apply
{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'ℂ}
(k : ℕ)
(f : source.Hom target)
(x : Vℂ)
:
Natural-number multiples of morphisms are evaluated pointwise on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.zsmul_apply
{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'ℂ}
(k : ℤ)
(f : source.Hom target)
(x : Vℂ)
:
Integer multiples of morphisms are evaluated pointwise on complex vectors.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.smul_apply
{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'ℂ}
(q : ℚ)
(f : source.Hom target)
(x : Vℂ)
:
Rational multiples of morphisms are evaluated pointwise on complex vectors, the scalar acting
through ℚ → ℂ.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.add_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g h : target.Hom third)
(f : source.Hom target)
:
Composition is additive in the morphism applied second.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_add
{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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f h : source.Hom target)
:
Composition is additive in the morphism applied first.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.smul_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(q : ℚ)
(g : target.Hom third)
(f : source.Hom target)
:
A rational multiple in the outer factor can be pulled out of a composition.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_smul
{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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(q : ℚ)
(f : source.Hom target)
:
A rational multiple in the inner factor can be pulled out of a composition.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.zero_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(f : source.Hom target)
:
Composing with a zero morphism on the left gives zero.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.comp_zero
{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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
:
Composing with a zero morphism on the right gives zero.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedMap
{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 : ℤ)
:
The map induced on the k-th rational graded piece grᵂ_k of the weight filtration.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedMap_mk
{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 : ℤ)
(x : ↥(source.WQ k))
:
The graded map sends the class of a vector to the class of its image.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.restrictWC
{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 : ℤ)
:
↥(rationalToComplexSubmodule hℚ hℂ (source.WQ k)) →ₗ[ℂ] ↥(rationalToComplexSubmodule h'ℚ h'ℂ (target.WQ k))
The restriction of the complex action to a step of the complexified weight filtration.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.coe_restrictWC_apply
{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 : ℤ)
(x : ↥(rationalToComplexSubmodule hℚ hℂ (source.WQ k)))
:
The restriction to a step of the complexified weight filtration acts by the complex action.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.complexGradedMap
{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 : ℤ)
:
weightGradedComplex (fun (j : ℤ) => rationalToComplexSubmodule hℚ hℂ (source.WQ j)) k →ₗ[ℂ] weightGradedComplex (fun (j : ℤ) => rationalToComplexSubmodule h'ℚ h'ℂ (target.WQ j)) k
The map induced on the k-th graded piece of the complexified weight filtration
TauCeti.Hodge.MixedHodgeStructure.WC, spelled out in the unfolded form in which
TauCeti.Hodge.gradedComplexEquiv presents that filtration.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.complexGradedMap_mk
{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 : ℤ)
(x : ↥(rationalToComplexSubmodule hℚ hℂ (source.WQ k)))
:
The complex graded map sends the class of a vector to the class of its image.
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedComplexEquiv_baseChange_gradedMap
{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 : ℤ)
(t : TensorProduct ℚ ℂ (weightGradedRat source.WQ k))
:
(gradedComplexEquiv h'ℚ h'ℂ target.WQ ⋯ k) ((LinearMap.baseChange ℂ (f.gradedMap k)) t) = (f.complexGradedMap k) ((gradedComplexEquiv hℚ hℂ source.WQ ⋯ k) t)
The comparison TauCeti.Hodge.gradedComplexEquiv is natural in the morphism: the square
formed by the two induced maps and that comparison commutes.
noncomputable def
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedHom
{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 : ℤ)
:
(source.gradedHodgeStructure k).Hom (target.gradedHodgeStructure k)
A morphism of mixed Hodge structures induces a morphism of the pure Hodge structures carried by the weight-graded pieces.
Instances For
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedHom_toIntLinearMap
{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 : ℤ)
:
The integral map underlying the induced morphism of pure Hodge structures is the graded map.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedMap_id
{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ℂ)
(k : ℤ)
:
The graded map of an identity morphism is the identity.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedMap_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
(k : ℤ)
:
The graded map of a composite is the composite of the graded maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.complexGradedMap_id
{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ℂ)
(k : ℤ)
:
The complex graded map of an identity morphism is the identity.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.complexGradedMap_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
(k : ℤ)
:
The complex graded map of a composite is the composite of the complex graded maps.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedHom_id
{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ℂ)
(k : ℤ)
:
Passage to the weight-graded pieces sends identities to identities.
@[simp]
theorem
TauCeti.Hodge.MixedHodgeStructure.Hom.gradedHom_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'ℂ}
{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 ℂ ι''ℂ}
{third : MixedHodgeStructure h''ℚ h''ℂ}
(g : target.Hom third)
(f : source.Hom target)
(k : ℤ)
:
Passage to the weight-graded pieces is compatible with composition.