Morphisms of pure Hodge structures #
A morphism between integral pure Hodge structures of the same weight is an integral linear map whose complexification preserves the Hodge filtration. The complex action is derived canonically from the integral map through the universal property of the source base change; in particular, it commutes with the lattice-induced conjugations.
Those two properties — commuting with the conjugations and preserving the filtration — are also
what a morphism of pure Hodge structures amounts to on the conjugation-parametric object
TauCeti.Hodge.HodgeStructureOn, where no lattice is in sight. They are recorded there as the
unbundled predicate TauCeti.Hodge.HodgeStructureOn.IsMorphism, from which the integral morphism
calculus below is derived: preservation of the filtration and compatibility with conjugation imply
preservation of the conjugate filtration and hence of every Hodge component H^{p,n-p}.
The rest of the file develops the elementary morphism calculus. Morphisms are closed under identities and composition, and form an additive commutative group.
Main declarations #
TauCeti.Hodge.HodgeStructureOn.IsMorphism: a complex-linear map commuting with the conjugations and preserving the Hodge filtration — a morphism of pure Hodge structures in unbundled, lattice-free form.TauCeti.Hodge.HodgeStructure.Hom: morphisms of integral pure Hodge structures of a fixed weight, withTauCeti.Hodge.HodgeStructure.Hom.isMorphismexhibiting one as such a map.TauCeti.Hodge.HodgeStructure.Hom.idandHom.comp: identity and composition.TauCeti.Hodge.HodgeStructure.Hom.map_conjF_le: morphisms preserve the conjugate filtration.TauCeti.Hodge.HodgeStructure.Hom.map_piece_le: morphisms preserve every Hodge component.
This supplies the morphism companion in Layer L0 of
TauCetiRoadmap/HodgeStructures/README.md. It follows the opposed-filtration convention of
Deligne, Théorie de Hodge II, §1.2.1, and the usual morphism convention in Voisin,
Hodge Theory and Complex Algebraic Geometry I, §7.
structure
TauCeti.Hodge.HodgeStructureOn.IsMorphism
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
(hs₁ : HodgeStructureOn W₁ ω₁ n)
(hs₂ : HodgeStructureOn W₂ ω₂ n)
(g : W₁ →ₗ[ℂ] W₂)
:
A morphism of pure Hodge structures of weight n, in unbundled form: a complex-linear map
commuting with the two conjugations and preserving every step of the Hodge filtration.
The bundled integral morphisms TauCeti.Hodge.HodgeStructure.Hom are of this form, by
TauCeti.Hodge.HodgeStructure.Hom.isMorphism.
The map commutes with the two conjugations.
The map preserves every step of the Hodge filtration.
Instances For
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.id
{W₁ : Type v₁}
[AddCommGroup W₁]
[Module ℂ W₁]
{ω₁ : Conjugation W₁}
{n : ℤ}
(hs : HodgeStructureOn W₁ ω₁ n)
:
hs.IsMorphism hs LinearMap.id
The identity map is a morphism of pure Hodge structures.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.comp
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g : W₁ →ₗ[ℂ] W₂}
{ω₃ : Conjugation W₃}
{hs₃ : HodgeStructureOn W₃ ω₃ n}
{g' : W₂ →ₗ[ℂ] W₃}
(h' : hs₂.IsMorphism hs₃ g')
(h : hs₁.IsMorphism hs₂ g)
:
hs₁.IsMorphism hs₃ (g' ∘ₗ g)
The composite of two morphisms of pure Hodge structures is a morphism.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.zero
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
:
hs₁.IsMorphism hs₂ 0
The zero map is a morphism of pure Hodge structures.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.add
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g g' : W₁ →ₗ[ℂ] W₂}
(h : hs₁.IsMorphism hs₂ g)
(h' : hs₁.IsMorphism hs₂ g')
:
hs₁.IsMorphism hs₂ (g + g')
The sum of two morphisms of pure Hodge structures is a morphism.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.neg
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g : W₁ →ₗ[ℂ] W₂}
(h : hs₁.IsMorphism hs₂ g)
:
hs₁.IsMorphism hs₂ (-g)
The negation of a morphism of pure Hodge structures is a morphism.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.sub
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g g' : W₁ →ₗ[ℂ] W₂}
(h : hs₁.IsMorphism hs₂ g)
(h' : hs₁.IsMorphism hs₂ g')
:
hs₁.IsMorphism hs₂ (g - g')
The difference of two morphisms of pure Hodge structures is a morphism.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.map_conjF_le
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g : W₁ →ₗ[ℂ] W₂}
(h : hs₁.IsMorphism hs₂ g)
(p : ℤ)
:
A morphism of pure Hodge structures preserves the conjugate Hodge filtration.
theorem
TauCeti.Hodge.HodgeStructureOn.IsMorphism.map_piece_le
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ω₁ : Conjugation W₁}
{ω₂ : Conjugation W₂}
{n : ℤ}
{hs₁ : HodgeStructureOn W₁ ω₁ n}
{hs₂ : HodgeStructureOn W₂ ω₂ n}
{g : W₁ →ₗ[ℂ] W₂}
(h : hs₁.IsMorphism hs₂ g)
(p : ℤ)
:
A morphism of pure Hodge structures preserves every Hodge component H^{p,n-p}.
structure
TauCeti.Hodge.HodgeStructure.Hom
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
(source : HodgeStructure h₁ n)
(target : HodgeStructure h₂ n)
:
Type (max u₁ u₂)
A morphism between integral pure Hodge structures of the same weight.
Its primary datum is an integral linear map. Its complexification is derived from the source
IsBaseChange witness together with the target integral inclusion, and is required to preserve
every step of the Hodge filtration.
The integral linear map underlying a Hodge morphism.
- map_mem_F (p : ℤ) (x : W₁) : x ∈ source.F p → (integralMapToComplex h₁ ι₂ self.toIntLinearMap) x ∈ target.F p
The complexification of the underlying map preserves every Hodge filtration step.
Instances For
noncomputable def
TauCeti.Hodge.HodgeStructure.Hom.toLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
The complex-linear map induced by an integral Hodge morphism.
Instances For
theorem
TauCeti.Hodge.HodgeStructure.Hom.toLinearMap_def
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
The complex action of a Hodge morphism is the complexification of its integral map. This is
the bridge to the TauCeti.Hodge.integralMapToComplex API.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instCoeFunForall
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
A Hodge morphism acts on complex vectors through the complexification of its integral map.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.apply_ι
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(x : V₁)
:
A Hodge morphism acts on integral vectors by its underlying integral map.
theorem
TauCeti.Hodge.HodgeStructure.Hom.ext
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{f g : source.Hom target}
(h : ∀ (x : V₁), f.toIntLinearMap x = g.toIntLinearMap x)
:
Two Hodge morphisms are equal when their integral maps agree on every vector.
theorem
TauCeti.Hodge.HodgeStructure.Hom.ext_iff
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{f g : source.Hom target}
:
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.commutes_conj
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(x : W₁)
:
The complex action of a Hodge morphism commutes with lattice-induced conjugation.
theorem
TauCeti.Hodge.HodgeStructure.Hom.map_F_le
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(p : ℤ)
:
Preservation of a filtration step in submodule-map form.
theorem
TauCeti.Hodge.HodgeStructure.Hom.isMorphism
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
HodgeStructureOn.IsMorphism source target f.toLinearMap
A bundled integral Hodge morphism is a morphism of the underlying pure Hodge structures.
theorem
TauCeti.Hodge.HodgeStructure.Hom.map_conjF_le
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(p : ℤ)
:
A Hodge morphism preserves the conjugate Hodge filtration.
theorem
TauCeti.Hodge.HodgeStructure.Hom.map_mem_conjF
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(p : ℤ)
{x : W₁}
(hx : x ∈ HodgeStructureOn.conjF source p)
:
Elementwise form of preservation of the conjugate Hodge filtration.
theorem
TauCeti.Hodge.HodgeStructure.Hom.map_piece_le
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(p : ℤ)
:
A Hodge morphism preserves every Hodge component H^{p,n-p}.
theorem
TauCeti.Hodge.HodgeStructure.Hom.map_mem_piece
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(p : ℤ)
{x : W₁}
(hx : x ∈ HodgeStructureOn.piece source p)
:
Elementwise form of preservation of Hodge components.
noncomputable def
TauCeti.Hodge.HodgeStructure.Hom.id
{V₁ : Type u₁}
{W₁ : Type v₁}
[AddCommGroup V₁]
[AddCommGroup W₁]
[Module ℂ W₁]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{h₁ : IsBaseChange ℂ ι₁}
{n : ℤ}
(source : HodgeStructure h₁ n)
:
source.Hom source
The identity morphism of an integral pure Hodge structure.
Instances For
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.id_toIntLinearMap
{V₁ : Type u₁}
{W₁ : Type v₁}
[AddCommGroup V₁]
[AddCommGroup W₁]
[Module ℂ W₁]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{h₁ : IsBaseChange ℂ ι₁}
{n : ℤ}
{source : HodgeStructure h₁ n}
:
The identity Hodge morphism acts as the identity on integral vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.id_apply
{V₁ : Type u₁}
{W₁ : Type v₁}
[AddCommGroup V₁]
[AddCommGroup W₁]
[Module ℂ W₁]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{h₁ : IsBaseChange ℂ ι₁}
{n : ℤ}
{source : HodgeStructure h₁ n}
(x : W₁)
:
The identity Hodge morphism acts as the identity on complex vectors.
noncomputable def
TauCeti.Hodge.HodgeStructure.Hom.comp
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g : target.Hom third)
(f : source.Hom target)
:
source.Hom third
Composition of morphisms of integral pure Hodge structures.
Instances For
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g : target.Hom third)
(f : source.Hom target)
:
The integral map underlying a composite is the composite of the integral maps.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g : target.Hom third)
(f : source.Hom target)
(x : W₁)
:
Composition of Hodge morphisms is pointwise composition on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.id_comp
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
Left identity law for Hodge morphisms.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_id
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
Right identity law for Hodge morphisms.
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_assoc
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
{V₄ : Type u_1}
{W₄ : Type u_2}
[AddCommGroup V₄]
[AddCommGroup W₄]
[Module ℂ W₄]
{ι₄ : V₄ →ₗ[ℤ] W₄}
{h₄ : IsBaseChange ℂ ι₄}
{fourth : HodgeStructure h₄ n}
(h : third.Hom fourth)
(g : target.Hom third)
(f : source.Hom target)
:
Associativity of composition of Hodge morphisms.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instZero
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
The zero morphism between two integral pure Hodge structures.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instAdd
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
Addition of Hodge morphisms, defined on their integral maps.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instNeg
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
Negation of a Hodge morphism, defined on its integral map.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instSub
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
Subtraction of Hodge morphisms, defined on their integral maps.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instSMulNat
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
Natural-number multiples of a Hodge morphism, defined on its integral map.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instSMulInt
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
Integer multiples of a Hodge morphism, defined on its integral map.
@[instance_reducible]
noncomputable instance
TauCeti.Hodge.HodgeStructure.Hom.instAddCommGroup
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
AddCommGroup (source.Hom target)
Integral Hodge morphisms form an additive commutative group, transported along the injection sending a morphism to its underlying integral linear map.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.zero_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
:
The zero Hodge morphism has the zero integral linear map underneath.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.add_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f g : source.Hom target)
:
Addition of Hodge morphisms is addition of their underlying integral linear maps.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.neg_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
:
Negation of a Hodge morphism is negation of its underlying integral linear map.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.sub_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f g : source.Hom target)
:
Subtraction of Hodge morphisms is subtraction of their underlying integral linear maps.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.nsmul_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(k : ℕ)
(f : source.Hom target)
:
Natural-number multiples of Hodge morphisms pass to their underlying integral linear maps.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.zsmul_toIntLinearMap
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(k : ℤ)
(f : source.Hom target)
:
Integer multiples of Hodge morphisms pass to their underlying integral linear maps.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.zero_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(x : W₁)
:
The zero Hodge morphism acts as zero on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.add_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f g : source.Hom target)
(x : W₁)
:
Addition of Hodge morphisms is pointwise addition on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.neg_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f : source.Hom target)
(x : W₁)
:
Negation of Hodge morphisms is pointwise negation on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.sub_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(f g : source.Hom target)
(x : W₁)
:
Subtraction of Hodge morphisms is pointwise subtraction on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.nsmul_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(k : ℕ)
(f : source.Hom target)
(x : W₁)
:
Natural-number multiples of Hodge morphisms are evaluated pointwise on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.zsmul_apply
{V₁ : Type u₁}
{V₂ : Type u₂}
{W₁ : Type v₁}
{W₂ : Type v₂}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
(k : ℤ)
(f : source.Hom target)
(x : W₁)
:
Integer multiples of Hodge morphisms are evaluated pointwise on complex vectors.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.add_comp
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g h : target.Hom third)
(f : source.Hom target)
:
Composition is additive in the morphism applied second.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_add
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g : target.Hom third)
(f h : source.Hom target)
:
Composition is additive in the morphism applied first.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.zero_comp
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(f : source.Hom target)
:
Composing with a zero morphism on the left gives zero.
@[simp]
theorem
TauCeti.Hodge.HodgeStructure.Hom.comp_zero
{V₁ : Type u₁}
{V₂ : Type u₂}
{V₃ : Type u₃}
{W₁ : Type v₁}
{W₂ : Type v₂}
{W₃ : Type v₃}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup W₁]
[Module ℂ W₁]
[AddCommGroup W₂]
[Module ℂ W₂]
[AddCommGroup W₃]
[Module ℂ W₃]
{ι₁ : V₁ →ₗ[ℤ] W₁}
{ι₂ : V₂ →ₗ[ℤ] W₂}
{ι₃ : V₃ →ₗ[ℤ] W₃}
{h₁ : IsBaseChange ℂ ι₁}
{h₂ : IsBaseChange ℂ ι₂}
{h₃ : IsBaseChange ℂ ι₃}
{n : ℤ}
{source : HodgeStructure h₁ n}
{target : HodgeStructure h₂ n}
{third : HodgeStructure h₃ n}
(g : target.Hom third)
:
Composing with a zero morphism on the right gives zero.