Documentation

TauCeti.Geometry.Hodge.Projection

Hodge projectors defined over ℚ #

A rational Hodge substructure of a polarizable pure Hodge structure is a direct summand of it as an object, not merely as a subspace: it is the image of an idempotent rational endomorphism whose complexification is a morphism of pure Hodge structures. That projector is the projection onto the rational subspace along its orthogonal complement for a polarizing form, and its complexification is the projection onto the complexified substructure along the complexified complement, because extension of scalars along ℚ → ℂ preserves idempotents, ranges and kernels. Being a morphism is then automatic: an idempotent endomorphism of the ambient complex space whose range and kernel are sub-Hodge structures commutes with the conjugation and preserves the Hodge filtration.

Conversely, the image and the kernel of any rational linear map whose complexification is a morphism of pure Hodge structures are rational Hodge substructures, with no polarization needed. So over a polarizable structure the rational Hodge substructures are exactly the images of the idempotent rational Hodge endomorphisms.

This sharpens the splitting of TauCeti.Hodge.exists_isCompl_of_isPolarizable, which produces a complementary rational subspace, into a splitting by endomorphisms of the Hodge structure itself: the semisimplicity of polarizable rational Hodge structures in the form that speaks about morphisms rather than about subspaces.

Following Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2.

Main declarations #

The projector onto a rational Hodge substructure #

source
noncomputable def TauCeti.Hodge.RationalHodgeSubstructure.projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
Vℚ →ₗ[ℚ] Vℚ

The Hodge projector onto a rational Hodge substructure for a chosen polarization: the projection onto its rational subspace along the orthogonal complement of that subspace.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.range_projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    (projection P W).range = W.WQ
    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.ker_projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    (projection P W).ker = (orthogonal P W).WQ
    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.isIdempotentElem_projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    IsIdempotentElem (projection P W)
    source
    theorem TauCeti.Hodge.RationalHodgeSubstructure.projection_eq_submodule_projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    projection P W = W.WQ.projection (orthogonal P W).WQ ⋯

    The Hodge projector is the submodule projection along the orthogonal complement.

    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.projection_apply_of_mem {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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) {x : Vℚ} (hx : x ∈ W.WQ) :
    (projection P W) x = x

    The Hodge projector fixes the rational Hodge substructure it projects onto.

    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.projection_apply_of_mem_orthogonal {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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) {x : Vℚ} (hx : ∀ y ∈ W.WQ, ((hℚ.bilinForm P.Qint) y) x = 0) :
    (projection P W) x = 0

    The Hodge projector annihilates the orthogonal complement it projects along.

    source
    theorem TauCeti.Hodge.RationalHodgeSubstructure.isMorphism_rationalMapToComplex_projection_of_isCompl {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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (W W' : RationalHodgeSubstructure hℚ hs) (h : IsCompl W W') :
    HodgeStructureOn.IsMorphism hs hs (rationalMapToComplex hℚ hℂ hℚ hℂ (W.WQ.projection W'.WQ ⋯))

    Projection along complementary rational Hodge substructures is a morphism of the ambient pure Hodge structure.

    source
    theorem TauCeti.Hodge.RationalHodgeSubstructure.isMorphism_rationalMapToComplex_projection {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    HodgeStructureOn.IsMorphism hs hs (rationalMapToComplex hℚ hℂ hℚ hℂ (projection P W))

    The complexification of the Hodge projector is a morphism of pure Hodge structures.

    source
    theorem TauCeti.Hodge.exists_isIdempotentElem_isMorphism_range_eq_of_isPolarizable {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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (h : IsPolarizable hℂ hs) (W : RationalHodgeSubstructure hℚ hs) :
    ∃ (e : Vℚ →ₗ[ℚ] Vℚ), IsIdempotentElem e ∧ HodgeStructureOn.IsMorphism hs hs (rationalMapToComplex hℚ hℂ hℚ hℂ e) ∧ e.range = W.WQ

    Semisimplicity of polarizable pure Hodge structures, in projector form. Every rational Hodge substructure of a polarizable pure Hodge structure is the image of an idempotent rational endomorphism whose complexification is a morphism of pure Hodge structures: the substructure is a direct summand as an object, split off by an endomorphism of the Hodge structure.

    source
    theorem TauCeti.Hodge.exists_isIdempotentElem_isMorphism_range_eq_iff {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} {hℚ : IsBaseChange ℚ ιℚ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (h : IsPolarizable hℂ hs) (A : Submodule ℚ Vℚ) :
    (∃ (e : Vℚ →ₗ[ℚ] Vℚ), IsIdempotentElem e ∧ HodgeStructureOn.IsMorphism hs hs (rationalMapToComplex hℚ hℂ hℚ hℂ e) ∧ e.range = A) ↔ ∃ (W : RationalHodgeSubstructure hℚ hs), W.WQ = A

    The rational Hodge substructures of a polarizable pure Hodge structure are exactly the images of the idempotent rational Hodge endomorphisms. The forward implication needs neither idempotency nor a polarization: the image of any rational Hodge morphism is a rational Hodge substructure.