Documentation

TauCeti.Geometry.Hodge.Mixed.Prod

Products of mixed Hodge structures #

The product of two mixed Hodge structures has componentwise weight and Hodge filtrations. The product of their Deligne bigradings witnesses purity on the weight-graded pieces. The two inclusions and projections are mixed Hodge morphisms; their rational maps are the usual inclusions and projections of vector spaces. Their binary bicone is a bilimit, giving binary biproducts and, together with the zero object, finite products in the category of mixed Hodge structures.

References #

Deligne, Théorie de Hodge II, §2.3; Peters–Steenbrink, Mixed Hodge Structures, Ch. 3.

source
noncomputable def TauCeti.Hodge.MixedHodgeStructure.prod {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
MixedHodgeStructure ⋯ ⋯

The product mixed Hodge structure, with componentwise weight and Hodge filtrations.

Instances For
    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.prod_WQ {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) (k : ℤ) :
    (X.prod Y).WQ k = (X.WQ k).prod (Y.WQ k)

    The weight filtration of the product is the product of the weight filtrations.

    source
    @[simp]
    theorem TauCeti.Hodge.MixedHodgeStructure.prod_F {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) (p : ℤ) :
    (X.prod Y).F p = (X.F p).prod (Y.F p)

    The Hodge filtration of the product is the product of the Hodge filtrations.

    source
    noncomputable def TauCeti.Hodge.MixedHodgeStructure.fst {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
    (X.prod Y).Hom X

    The first projection from the product mixed Hodge structure.

    Instances For
      source
      noncomputable def TauCeti.Hodge.MixedHodgeStructure.snd {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
      (X.prod Y).Hom Y

      The second projection from the product mixed Hodge structure.

      Instances For
        source
        noncomputable def TauCeti.Hodge.MixedHodgeStructure.inl {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
        X.Hom (X.prod Y)

        The first inclusion into the product mixed Hodge structure.

        Instances For
          source
          noncomputable def TauCeti.Hodge.MixedHodgeStructure.inr {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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
          Y.Hom (X.prod Y)

          The second inclusion into the product mixed Hodge structure.

          Instances For
            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.fst_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.fst Y).toRatLinearMap = LinearMap.fst ℚ Vℚ V'ℚ

            The rational map of the first projection is the usual first projection of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.snd_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.snd Y).toRatLinearMap = LinearMap.snd ℚ Vℚ V'ℚ

            The rational map of the second projection is the usual second projection of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.inl_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.inl Y).toRatLinearMap = LinearMap.inl ℚ Vℚ V'ℚ

            The rational map of the first inclusion is the usual first inclusion of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.inr_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.inr Y).toRatLinearMap = LinearMap.inr ℚ Vℚ V'ℚ

            The rational map of the second inclusion is the usual second inclusion of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.fst_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.fst Y).toLinearMap = LinearMap.fst ℂ Vℂ V'ℂ

            The complex map of the first projection is the usual first projection of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.snd_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.snd Y).toLinearMap = LinearMap.snd ℂ Vℂ V'ℂ

            The complex map of the second projection is the usual second projection of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.inl_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.inl Y).toLinearMap = LinearMap.inl ℂ Vℂ V'ℂ

            The complex map of the first inclusion is the usual first inclusion of vector spaces.

            source
            @[simp]
            theorem TauCeti.Hodge.MixedHodgeStructure.inr_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 ℂ ι'ℂ} (X : MixedHodgeStructure hℚ hℂ) (Y : MixedHodgeStructure h'ℚ h'ℂ) :
            (X.inr Y).toLinearMap = LinearMap.inr ℂ Vℂ V'ℂ

            The complex map of the second inclusion is the usual second inclusion of vector spaces.

            source
            instance TauCeti.Hodge.MixedHodgeStructureCat.hasBinaryBiproducts :
            CategoryTheory.Limits.HasBinaryBiproducts MixedHodgeStructureCat
            source
            instance TauCeti.Hodge.MixedHodgeStructureCat.hasFiniteProducts :
            CategoryTheory.Limits.HasFiniteProducts MixedHodgeStructureCat