Documentation

TauCeti.Geometry.Hodge.InducedPolarization

Polarizations on rational Hodge substructures #

A rational Hodge substructure inherits a pure Hodge structure on its rational and complex base-change models. If the ambient structure is polarized, restricting the integral form to the integral vectors in the rational subspace polarizes this induced structure.

The only substantive point is nondegeneracy. Hodge--Riemann positivity makes a rational Hodge substructure disjoint from its orthogonal complement, so the complex polarizing form restricts nondegenerately. Nondegeneracy then descends to the restricted integral form.

This construction supplies the objects represented by rational Hodge substructures in the category of polarizable rational Hodge structures. It follows the orthogonal-complement argument of Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters--Steenbrink, Mixed Hodge Structures, §2.

Main declarations #

source
noncomputable def TauCeti.Hodge.RationalHodgeSubstructure.hodgeStructure {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 : RationalHodgeSubstructure hℚ hs) :
HodgeStructure ⋯ n

The pure Hodge structure induced on a rational Hodge substructure. Its integral carrier is the lattice of integral vectors lying in W.WQ, its rational carrier is W.WQ, and its complex carrier is W.WC.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.hodgeStructure_F {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 : RationalHodgeSubstructure hℚ hs) (p : ℤ) :
    W.hodgeStructure.F p = Submodule.comap (rationalToComplexSubmodule hℚ hℂ W.WQ).subtype (hs.F p)

    The filtration on the induced Hodge structure is the trace of the ambient filtration.

    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.hodgeStructure_conjF {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 : RationalHodgeSubstructure hℚ hs) (p : ℤ) :
    HodgeStructureOn.conjF W.hodgeStructure p = Submodule.comap (rationalToComplexSubmodule hℚ hℂ W.WQ).subtype (HodgeStructureOn.conjF hs p)

    The conjugate filtration on the induced structure is the trace of the ambient conjugate filtration.

    source
    @[simp]
    theorem TauCeti.Hodge.RationalHodgeSubstructure.hodgeStructure_piece {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 : RationalHodgeSubstructure hℚ hs) (p : ℤ) :
    HodgeStructureOn.piece W.hodgeStructure p = Submodule.comap (rationalToComplexSubmodule hℚ hℂ W.WQ).subtype (HodgeStructureOn.piece hs p)

    The Hodge components of the induced structure are the traces of the ambient components.

    source
    theorem TauCeti.Hodge.RationalHodgeSubstructure.isMorphism_subtype {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 : RationalHodgeSubstructure hℚ hs) :
    HodgeStructureOn.IsMorphism W.hodgeStructure hs (rationalToComplexSubmodule hℚ hℂ W.WQ).subtype

    The inclusion of a rational Hodge substructure into its ambient complex space is a morphism of pure Hodge structures.

    source
    def TauCeti.Hodge.RationalHodgeSubstructure.inducedForm {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
    LinearMap.BilinForm ℤ ↥(integralSubmodule ιℚ W.WQ)

    The integral polarizing form restricted to the integral vectors of a rational Hodge substructure.

    Instances For
      source
      @[simp]
      theorem TauCeti.Hodge.RationalHodgeSubstructure.inducedForm_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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (W : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) (x y : ↥(integralSubmodule ιℚ W.WQ)) :
      ((W.inducedForm P) x) y = (P.Qint ↑x) ↑y

      The restricted integral form evaluates as the ambient integral form on underlying vectors.

      source
      theorem TauCeti.Hodge.RationalHodgeSubstructure.bilinForm_inducedForm {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
      ⋯.bilinForm (W.inducedForm P) = P.Q.restrict (rationalToComplexSubmodule hℚ hℂ W.WQ)

      The complexification of the restricted integral form is the restriction of the ambient complex polarizing form.

      source
      theorem TauCeti.Hodge.RationalHodgeSubstructure.inducedForm_nondegenerate {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
      (W.inducedForm P).Nondegenerate

      The restricted integral form is nondegenerate.

      source
      noncomputable def TauCeti.Hodge.RationalHodgeSubstructure.inducedPolarization {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
      Polarization ⋯ W.hodgeStructure

      Restricting a polarization to a rational Hodge substructure gives a polarization of its induced Hodge structure.

      Instances For
        source
        @[simp]
        theorem TauCeti.Hodge.RationalHodgeSubstructure.inducedPolarization_Qint {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
        (W.inducedPolarization P).Qint = W.inducedForm P

        The integral form underlying the induced polarization is the restricted ambient form.

        source
        @[simp]
        theorem TauCeti.Hodge.RationalHodgeSubstructure.inducedPolarization_Q {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 : RationalHodgeSubstructure hℚ hs) (P : Polarization hℂ hs) :
        (W.inducedPolarization P).Q = P.Q.restrict (rationalToComplexSubmodule hℚ hℂ W.WQ)

        The complex form underlying the induced polarization is the restricted ambient complex form.

        source
        theorem TauCeti.Hodge.RationalHodgeSubstructure.isPolarizable_hodgeStructure {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 : RationalHodgeSubstructure hℚ hs) (hpol : IsPolarizable hℂ hs) :
        IsPolarizable ⋯ W.hodgeStructure

        A rational Hodge substructure of a polarizable pure Hodge structure is polarizable.