Sub-Hodge structures and the strictness of Hodge morphisms

A subspace of the ambient complex vector space of a pure Hodge structure is a sub-Hodge structure when it is stable under the conjugation and is spanned by its intersections with the Hodge components. Such a subspace inherits a pure Hodge structure of the same weight, namely the ambient filtration intersected with it: opposedness survives because the two complementary ambient steps already cover the subspace componentwise.

The two conditions are equivalent to conjugation stability together with stability under the Hodge projections, and that reformulation is what makes the subobjects of the theory easy to recognise. It is used here to identify the kernel and the image of a morphism of pure Hodge structures as sub-Hodge structures — and, dually, the quotient by a sub-Hodge structure as a pure Hodge structure again, so that the cokernel of a morphism is one — and then to prove that a morphism of pure Hodge structures is strict: its image meets every step of the target filtration exactly in the image of that step,

range f ⊓ F'^p = f (F^p),

and likewise componentwise, range f ⊓ H'^{p,n-p} = f (H^{p,n-p}). The mechanism is that a morphism intertwines the Hodge projections of source and target, so it is a graded map for the two Hodge decompositions; strictness is then bookkeeping on degrees.

Dually, a sub-Hodge structure that admits a complementary sub-Hodge structure is cut out by an endomorphism of the Hodge structure itself: an idempotent endomorphism of the ambient complex vector space whose range and kernel are sub-Hodge structures is automatically a morphism, and the Hodge components split along the resulting decomposition.

Statements are given for the conjugation-parametric object HodgeStructureOn and for the unbundled morphism predicate TauCeti.Hodge.HodgeStructureOn.IsMorphism. The bundled integral morphisms of TauCeti.Hodge.HodgeStructure.Hom satisfy that predicate, so every result specialises to them.

These are the subobject companions of Layers L0 and L1 of TauCetiRoadmap/HodgeStructures/README.md: the kernel and image of a Hodge morphism are the subobjects a categorical reading of the semisimplicity of polarizable rational Hodge structures quantifies over, and strictness for a pure structure is the graded shadow of Deligne's strictness theorem for mixed Hodge structures. Following Peters–Steenbrink, Mixed Hodge Structures, §2.1, and Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.IsSubstructure: a conjugation-stable subspace spanned by its intersections with the Hodge components.
• TauCeti.Hodge.HodgeStructureOn.isSubstructure_iff_proj_mem: equivalently, a conjugation-stable subspace stable under the Hodge projections.
• TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure: the pure Hodge structure induced on a sub-Hodge structure, with components the intersections with the ambient components.
• TauCeti.Hodge.HodgeStructureOn.IsSubstructure.quotient: the pure Hodge structure induced on the quotient by a sub-Hodge structure, with components the images of the ambient components; applied to the image of a morphism it is the cokernel.
• TauCeti.Hodge.HodgeStructureOn.IsMorphism.proj_comp: a morphism of pure Hodge structures intertwines the Hodge projections.
• TauCeti.Hodge.HodgeStructureOn.IsMorphism.isSubstructure_ker and …isSubstructure_range: the kernel and the image of a morphism are sub-Hodge structures.
• TauCeti.Hodge.HodgeStructureOn.IsMorphism.range_inf_F: strictness, range f ⊓ F'^p is the image of F^p; …range_inf_piece and …range_inf_conjF are the componentwise and conjugate forms.
• TauCeti.Hodge.HodgeStructureOn.isMorphism_of_isIdempotentElem: an idempotent endomorphism whose range and kernel are sub-Hodge structures is a morphism of pure Hodge structures; …IsSubstructure.isMorphism_projection is the projection onto a sub-Hodge structure along a complementary one.
• TauCeti.Hodge.HodgeStructureOn.IsSubstructure.piece_eq_sup: each Hodge component is the sum of its intersections with two complementary sub-Hodge structures.

Sub-Hodge structures

structure TauCeti.Hodge.HodgeStructureOn.IsSubstructure {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (U : Submodule ℂ W) : Prop

A sub-Hodge structure of a pure Hodge structure: a complex subspace stable under the conjugation and spanned by its intersections with the Hodge components.

The reverse inequality ⨆ p, U ⊓ hs.piece p ≤ U holds for any subspace, so the second field is the whole of the spanning condition; see TauCeti.Hodge.HodgeStructureOn.IsSubstructure.eq_iSup_inf_piece.

• conj_mem (x : W) : x ∈ U → ω.toEquiv x ∈ U

  The subspace is stable under the conjugation.

• le_iSup_inf_piece : U ≤ ⨆ (p : ℤ), U ⊓ hs.piece p

  The subspace is spanned by its intersections with the Hodge components.

theorem TauCeti.Hodge.HodgeStructureOn.isSubstructure_of_proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (hconj : ∀ x ∈ U, ω.toEquiv x ∈ U) (hproj : ∀ (p : ℤ), ∀ x ∈ U, (hs.proj p) x ∈ U) : hs.IsSubstructure U

A conjugation-stable subspace stable under the Hodge projections is a sub-Hodge structure.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.eq_iSup_inf_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : U = ⨆ (p : ℤ), U ⊓ hs.piece p

A sub-Hodge structure is the sum of its intersections with the Hodge components.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) {x : W} (hx : x ∈ U) (p : ℤ) : (hs.proj p) x ∈ U

A sub-Hodge structure is stable under the Hodge projections.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.map_conj {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : Submodule.map (↑ω.toEquiv) U = U

Conjugation maps a sub-Hodge structure onto itself.

noncomputable def TauCeti.Hodge.HodgeStructureOn.IsSubstructure.conjugation {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : Conjugation ↥U

The conjugation induced on a sub-Hodge structure.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.conjugation_toEquiv_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (x : ↥U) : ↑(h.conjugation.toEquiv x) = ω.toEquiv ↑x

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.le_inf_F_sup_inf_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : U ≤ U ⊓ hs.F p ⊔ U ⊓ hs.conjF (n + 1 - p)

A filtration step and the complementary conjugate step cover a sub-Hodge structure: each of its Hodge components lies in one of the two.

noncomputable def TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : HodgeStructureOn (↥U) h.conjugation n

The pure Hodge structure induced on a sub-Hodge structure: its filtration is the ambient filtration intersected with the subspace, and it is opposed because the ambient components already cover the subspace.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.hodgeStructure.F p = Submodule.comap U.subtype (hs.F p)

The induced Hodge filtration is the ambient filtration intersected with the subspace.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.hodgeStructure.conjF p = Submodule.comap U.subtype (hs.conjF p)

The induced conjugate filtration is the ambient conjugate filtration intersected with the subspace.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.hodgeStructure_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.hodgeStructure.piece p = Submodule.comap U.subtype (hs.piece p)

An induced Hodge component is the ambient component of the same degree intersected with the subspace.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.isMorphism_subtype {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : h.hodgeStructure.IsMorphism hs U.subtype

The inclusion of a sub-Hodge structure into its ambient Hodge structure is a morphism.

Quotients by a sub-Hodge structure

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.map_quotient_conj_map_mkQ {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (A : Submodule ℂ W) : Submodule.map (↑(ω.quotient ⋯).toEquiv) (Submodule.map U.mkQ A) = Submodule.map U.mkQ (Submodule.map (↑ω.toEquiv) A)

Conjugating in the quotient by a sub-Hodge structure is conjugating upstairs.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.F_inf_conjF_sup_le {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : hs.F p ⊓ (hs.conjF (n + 1 - p) ⊔ U) ≤ U

A filtration step meets the sum of the complementary conjugate step with a sub-Hodge structure inside that sub-Hodge structure: this is what makes opposedness descend to the quotient.

noncomputable def TauCeti.Hodge.HodgeStructureOn.IsSubstructure.quotient {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : HodgeStructureOn (W ⧸ U) (ω.quotient ⋯) n

The pure Hodge structure induced on the quotient by a sub-Hodge structure: its filtration is the image of the ambient filtration. Opposedness descends because the sub-Hodge structure is itself split by the two complementary ambient steps.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.quotient_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.quotient.F p = Submodule.map U.mkQ (hs.F p)

The filtration of the quotient Hodge structure is the image of the ambient filtration.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.quotient_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.quotient.conjF p = Submodule.map U.mkQ (hs.conjF p)

The conjugate filtration of the quotient Hodge structure is the image of the ambient conjugate filtration.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.isMorphism_liftQ {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsSubstructure U) (hg : hs.IsMorphism hs' g) (hU : U ≤ g.ker) : h.quotient.IsMorphism hs' (U.liftQ g hU)

A morphism killing a sub-Hodge structure descends to a morphism from the quotient.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.existsUnique_isMorphism_liftQ {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsSubstructure U) (hg : hs.IsMorphism hs' g) (hU : U ≤ g.ker) : ∃! q : W ⧸ U →ₗ[ℂ] W', h.quotient.IsMorphism hs' q ∧ q ∘ₗ U.mkQ = g

The descended Hodge morphism is the unique one whose composite with the quotient map is the original morphism.

theorem TauCeti.Hodge.HodgeStructureOn.isSubstructure_iff_proj_mem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} : hs.IsSubstructure U ↔ (∀ x ∈ U, ω.toEquiv x ∈ U) ∧ ∀ (p : ℤ), ∀ x ∈ U, (hs.proj p) x ∈ U

A subspace is a sub-Hodge structure exactly when it is stable under the conjugation and under every Hodge projection.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.isSubstructure_bot {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} : hs.IsSubstructure ⊥

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.isSubstructure_top {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} : hs.IsSubstructure ⊤

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.inf {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U U' : Submodule ℂ W} (h : hs.IsSubstructure U) (h' : hs.IsSubstructure U') : hs.IsSubstructure (U ⊓ U')

Sub-Hodge structures are closed under intersection.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.sup {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U U' : Submodule ℂ W} (h : hs.IsSubstructure U) (h' : hs.IsSubstructure U') : hs.IsSubstructure (U ⊔ U')

Sub-Hodge structures are closed under sum.

Morphisms of pure Hodge structures

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.proj_comp {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) (p : ℤ) : hs'.proj p ∘ₗ g = g ∘ₗ hs.proj p

A morphism of pure Hodge structures is graded: it intertwines the Hodge projections of the source and of the target.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.proj_apply {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) (p : ℤ) (x : W) : (hs'.proj p) (g x) = g ((hs.proj p) x)

Elementwise form of gradedness: the p-th projection of an image is the image of the p-th projection.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.isSubstructure_ker {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) : hs.IsSubstructure g.ker

The kernel of a morphism of pure Hodge structures is a sub-Hodge structure.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.isSubstructure_range {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) : hs'.IsSubstructure g.range

The image of a morphism of pure Hodge structures is a sub-Hodge structure.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.range_inf_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) (p : ℤ) : g.range ⊓ hs'.piece p = Submodule.map g (hs.piece p)

Componentwise strictness. The image of a morphism meets a Hodge component of the target exactly in the image of the corresponding component of the source.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.range_inf_F {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) (p : ℤ) : g.range ⊓ hs'.F p = Submodule.map g (hs.F p)

Strictness of a morphism of pure Hodge structures. The image meets a step of the target Hodge filtration exactly in the image of that step of the source filtration.

theorem TauCeti.Hodge.HodgeStructureOn.IsMorphism.range_inf_conjF {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {W' : Type v} [AddCommGroup W'] [Module ℂ W'] {ω' : Conjugation W'} {hs' : HodgeStructureOn W' ω' n} {g : W →ₗ[ℂ] W'} (h : hs.IsMorphism hs' g) (p : ℤ) : g.range ⊓ hs'.conjF p = Submodule.map g (hs.conjF p)

Conjugate strictness. The image meets a step of the conjugate target filtration exactly in the image of the corresponding step of the source.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.isMorphism_mkQ {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) : hs.IsMorphism h.quotient U.mkQ

The quotient map onto the Hodge structure of a quotient by a sub-Hodge structure is a morphism of pure Hodge structures.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.quotient_piece {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U : Submodule ℂ W} (h : hs.IsSubstructure U) (p : ℤ) : h.quotient.piece p = Submodule.map U.mkQ (hs.piece p)

The Hodge components of a quotient by a sub-Hodge structure are the images of the ambient components: the quotient map is strict, so its componentwise strictness identifies them.

Idempotent splittings

An idempotent endomorphism of the ambient complex vector space whose range and kernel are both sub-Hodge structures is automatically a morphism of pure Hodge structures, so a sub-Hodge structure with a complementary sub-Hodge structure is cut out by an endomorphism of the Hodge structure itself. The Hodge decomposition is then compatible with the splitting: each Hodge component is the sum of its intersections with the two pieces.

theorem TauCeti.Hodge.HodgeStructureOn.map_piece_le_of_isIdempotentElem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {e : W →ₗ[ℂ] W} (he : IsIdempotentElem e) (hrange : hs.IsSubstructure e.range) (hker : hs.IsSubstructure e.ker) (q : ℤ) : Submodule.map e (hs.piece q) ≤ hs.piece q

An idempotent endomorphism whose range and kernel are sub-Hodge structures maps every Hodge component into itself: on a component, the two summands of a vector are again of that degree.

theorem TauCeti.Hodge.HodgeStructureOn.isMorphism_of_isIdempotentElem {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {e : W →ₗ[ℂ] W} (he : IsIdempotentElem e) (hrange : hs.IsSubstructure e.range) (hker : hs.IsSubstructure e.ker) : hs.IsMorphism hs e

An idempotent endomorphism whose range and kernel are sub-Hodge structures is a morphism of pure Hodge structures.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.isMorphism_projection {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U U' : Submodule ℂ W} (hU : hs.IsSubstructure U) (hU' : hs.IsSubstructure U') (h : IsCompl U U') : hs.IsMorphism hs (U.projection U' h)

The projection onto a sub-Hodge structure along a complementary sub-Hodge structure is a morphism of pure Hodge structures, so a split sub-Hodge structure is the image of an idempotent endomorphism of the Hodge structure.

theorem TauCeti.Hodge.HodgeStructureOn.IsSubstructure.piece_eq_sup {W : Type u} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} {hs : HodgeStructureOn W ω n} {U U' : Submodule ℂ W} (hU : hs.IsSubstructure U) (hU' : hs.IsSubstructure U') (h : IsCompl U U') (q : ℤ) : hs.piece q = U ⊓ hs.piece q ⊔ U' ⊓ hs.piece q

The Hodge decomposition is compatible with a splitting into sub-Hodge structures: each Hodge component is the sum of its intersections with two complementary sub-Hodge structures.

Bundled integral morphisms

theorem TauCeti.Hodge.HodgeStructure.Hom.isSubstructure_ker {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.IsSubstructure source f.toLinearMap.ker

The kernel of an integral Hodge morphism is a sub-Hodge structure of the source.

theorem TauCeti.Hodge.HodgeStructure.Hom.isSubstructure_range {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.IsSubstructure target f.toLinearMap.range

The image of an integral Hodge morphism is a sub-Hodge structure of the target.

theorem TauCeti.Hodge.HodgeStructure.Hom.range_inf_F {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 : ℤ) : f.toLinearMap.range ⊓ target.F p = Submodule.map f.toLinearMap (source.F p)

Strictness of an integral Hodge morphism.

theorem TauCeti.Hodge.HodgeStructure.Hom.range_inf_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 : ℤ) : f.toLinearMap.range ⊓ HodgeStructureOn.piece target p = Submodule.map f.toLinearMap (HodgeStructureOn.piece source p)

Componentwise strictness of an integral Hodge morphism.

theorem TauCeti.Hodge.HodgeStructure.Hom.range_inf_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 : ℤ) : f.toLinearMap.range ⊓ HodgeStructureOn.conjF target p = Submodule.map f.toLinearMap (HodgeStructureOn.conjF source p)

Conjugate strictness of an integral Hodge morphism.