The category of polarizable rational Hodge structures

This file bundles polarizable pure Hodge structures of a fixed weight whose integral, rational, and complex models live in one universe. Morphisms are rational linear maps whose complexifications preserve the Hodge filtration. Thus the polarization is a property of an object, not chosen data, and morphisms are ordinary Hodge morphisms rather than isometries.

The resulting category is preadditive and ℚ-linear. Its rational realization is a faithful ℚ-linear functor to ModuleCat ℚ, and its complex realization is a ℚ-linear functor to ModuleCat ℂ. This category is the setting for formulating semisimplicity and splitting Hodge projectors on rational Hodge substructures.

The implementation specializes the existing mixed-Hodge category: a pure object is sent to MixedHodgeStructure.ofPure, and its morphisms and categorical structure are inherited from MixedHodgeStructureCat.

Main declarations

• TauCeti.Hodge.PolarizableHodgeStructureCat: polarizable rational Hodge structures of a fixed weight.
• TauCeti.Hodge.PolarizableHodgeStructureCat.Hom: ordinary rational Hodge morphisms.
• TauCeti.Hodge.PolarizableHodgeStructureCat.mixed: the fully faithful realization as mixed Hodge structures.
• TauCeti.Hodge.PolarizableHodgeStructureCat.rational: the faithful rational realization.
• TauCeti.Hodge.PolarizableHodgeStructureCat.complex: the complex realization.

References

The formal construction specializes TauCeti.Geometry.Hodge.Mixed.Category, in particular TauCeti.Hodge.MixedHodgeStructureCat. For the mathematics, see Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters--Steenbrink, Mixed Hodge Structures, §2.

structure TauCeti.Hodge.PolarizableHodgeStructureCat (n : ℤ) : Type (u + 1)

The category of finite-dimensional polarizable rational Hodge structures of weight n, with integral, rational, and complex models in Type u.

The integral model is a finitely generated free lattice and determines the conjugation on the complexification. The rational model is the carrier on which morphisms are defined. Polarizability is retained only as a property, so no particular polarizing form is part of an object.

• intCarrier : Type u

  The integral lattice underlying the Hodge structure.

• ratCarrier : Type u

  The rational vector space underlying the Hodge structure.

• complexCarrier : Type u

  The complex vector space underlying the Hodge structure.

• intAddCommGroup : AddCommGroup self.intCarrier

  The additive group structure on the integral lattice.

• intFree : Module.Free ℤ self.intCarrier

  The integral lattice is free.

• intFinite : Module.Finite ℤ self.intCarrier

  The integral lattice is finitely generated.

• ratAddCommGroup : AddCommGroup self.ratCarrier

  The additive group structure on the rational carrier.

• ratModule : Module ℚ self.ratCarrier

  The rational module structure.

• ratFinite : Module.Finite ℚ self.ratCarrier

  The rational carrier is finite-dimensional.

• complexAddCommGroup : AddCommGroup self.complexCarrier

  The additive group structure on the complex carrier.

• complexModule : Module ℂ self.complexCarrier

  The complex module structure.

• toRat : self.intCarrier →ₗ[ℤ] self.ratCarrier

  The structure map from the integral lattice to the rational model.

• toComplex : self.intCarrier →ₗ[ℤ] self.complexCarrier

  The structure map from the integral lattice to the complex model.

• isBaseChangeRat : IsBaseChange ℚ self.toRat

  The rational model is a base change of the integral lattice.

• isBaseChangeComplex : IsBaseChange ℂ self.toComplex

  The complex model is a base change of the integral lattice.

• hs : HodgeStructure ⋯ n

  The pure Hodge structure on the complexification.

• isPolarizable : IsPolarizable ⋯ self.hs

  The Hodge structure admits a polarization.

@[reducible, inline]

abbrev TauCeti.Hodge.PolarizableHodgeStructureCat.of {n : ℤ} {Vℤ Vℚ Vℂ : Type u} [AddCommGroup Vℤ] [Module.Free ℤ Vℤ] [Module.Finite ℤ Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [Module.Finite ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (hs : HodgeStructure hℂ n) (hpol : IsPolarizable hℂ hs) : PolarizableHodgeStructureCat n

Bundle a finite-dimensional polarizable rational Hodge structure as an object.

@[reducible, inline]

abbrev TauCeti.Hodge.PolarizableHodgeStructureCat.rat {n : ℤ} (X : PolarizableHodgeStructureCat n) : ModuleCat ℚ

The rational vector space underlying a polarizable rational Hodge structure.

@[reducible, inline]

abbrev TauCeti.Hodge.PolarizableHodgeStructureCat.complexSpace {n : ℤ} (X : PolarizableHodgeStructureCat n) : ModuleCat ℂ

The complex vector space underlying a polarizable rational Hodge structure.

@[reducible, inline]

noncomputable abbrev TauCeti.Hodge.PolarizableHodgeStructureCat.asMixed {n : ℤ} (X : PolarizableHodgeStructureCat n) : MixedHodgeStructureCat

A polarizable pure Hodge structure regarded as a mixed Hodge structure concentrated in its weight.

@[instance_reducible]

noncomputable instance TauCeti.Hodge.PolarizableHodgeStructureCat.instCategory {n : ℤ} : CategoryTheory.Category.{u, u + 1} (PolarizableHodgeStructureCat n)

@[reducible, inline]

abbrev TauCeti.Hodge.PolarizableHodgeStructureCat.Hom {n : ℤ} (X Y : PolarizableHodgeStructureCat n) : Type u

An ordinary morphism of polarizable rational Hodge structures, implemented as a morphism of the corresponding pure mixed Hodge structures. The concentrated weight condition is automatic.

@[instance_reducible]

noncomputable instance TauCeti.Hodge.PolarizableHodgeStructureCat.instCoeFunHomForallComplexCarrier {n : ℤ} {X Y : PolarizableHodgeStructureCat n} : CoeFun (X.Hom Y) fun (x : X.Hom Y) => X.complexCarrier → Y.complexCarrier

A morphism of polarizable Hodge structures acts through its complexification.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.mk {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : ∀ (p : ℤ), ∀ x ∈ X.hs.F p, (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f) x ∈ Y.hs.F p) : X.Hom Y

Construct a morphism from a rational linear map whose complexification preserves the Hodge filtration. Preservation of the concentrated weight filtration is automatic.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.mk_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : ∀ (p : ℤ), ∀ x ∈ X.hs.F p, (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f) x ∈ Y.hs.F p) : (mk f hf).hom.toRatLinearMap = f

The constructor retains the supplied rational linear map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.mk_toLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : ∀ (p : ℤ), ∀ x ∈ X.hs.F p, (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f) x ∈ Y.hs.F p) : MixedHodgeStructure.Hom.toLinearMap (mk f hf).hom = rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f

The complex map of the constructed morphism is the complexification of the supplied rational linear map.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.ofIsMorphism {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : HodgeStructureOn.IsMorphism X.hs Y.hs (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f)) : X.Hom Y

Construct a morphism from a rational linear map whose complexification is a morphism of the underlying pure Hodge structures.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.ofIsMorphism_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : HodgeStructureOn.IsMorphism X.hs Y.hs (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f)) : (ofIsMorphism f hf).hom.toRatLinearMap = f

The constructor from an unbundled Hodge morphism retains the supplied rational linear map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.ofIsMorphism_toLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : HodgeStructureOn.IsMorphism X.hs Y.hs (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f)) : MixedHodgeStructure.Hom.toLinearMap (ofIsMorphism f hf).hom = rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f

The complex map of the morphism built from an unbundled Hodge morphism is the complexification of the supplied rational linear map.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.isMorphism {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X.Hom Y) : HodgeStructureOn.IsMorphism X.hs Y.hs (MixedHodgeStructure.Hom.toLinearMap f.hom)

A rational Hodge morphism is a morphism of the underlying pure Hodge structures on the complexifications.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.ext {n : ℤ} {X Y : PolarizableHodgeStructureCat n} {f g : X ⟶ Y} (h : f.hom.toRatLinearMap = g.hom.toRatLinearMap) : f = g

Two categorical morphisms agree if their rational maps agree.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.Hom.ext_iff {n : ℤ} {X Y : PolarizableHodgeStructureCat n} {f g : X ⟶ Y} : f = g ↔ f.hom.toRatLinearMap = g.hom.toRatLinearMap

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.id_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) : (CategoryTheory.CategoryStruct.id X).hom.toRatLinearMap = LinearMap.id

The categorical identity has the identity rational linear map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.comp_toRatLinearMap {n : ℤ} {X Y Z : PolarizableHodgeStructureCat n} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom.toRatLinearMap = g.hom.toRatLinearMap ∘ₗ f.hom.toRatLinearMap

Categorical composition is composition of the underlying rational linear maps.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.id_toLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) : MixedHodgeStructure.Hom.toLinearMap (CategoryTheory.CategoryStruct.id X).hom = LinearMap.id

The identity morphism has the identity complex linear map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.comp_toLinearMap {n : ℤ} {X Y Z : PolarizableHodgeStructureCat n} (f : X ⟶ Y) (g : Y ⟶ Z) : MixedHodgeStructure.Hom.toLinearMap (CategoryTheory.CategoryStruct.comp f g).hom = MixedHodgeStructure.Hom.toLinearMap g.hom ∘ₗ MixedHodgeStructure.Hom.toLinearMap f.hom

Composition of categorical morphisms is composition of their complex linear maps.

@[instance_reducible]

noncomputable instance TauCeti.Hodge.PolarizableHodgeStructureCat.instPreadditive {n : ℤ} : CategoryTheory.Preadditive (PolarizableHodgeStructureCat n)

@[instance_reducible]

noncomputable instance TauCeti.Hodge.PolarizableHodgeStructureCat.instLinearRat {n : ℤ} : CategoryTheory.Linear ℚ (PolarizableHodgeStructureCat n)

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.zero_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} : (CategoryTheory.InducedCategory.Hom.hom 0).toRatLinearMap = 0

The zero morphism has the zero rational linear map underneath.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.add_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f g : X ⟶ Y) : (f + g).hom.toRatLinearMap = f.hom.toRatLinearMap + g.hom.toRatLinearMap

Addition of morphisms is addition of their underlying rational linear maps.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.smul_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (q : ℚ) (f : X ⟶ Y) : (q • f).hom.toRatLinearMap = q • f.hom.toRatLinearMap

Rational scalar multiplication passes to the underlying rational linear map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.zero_toLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} : MixedHodgeStructure.Hom.toLinearMap (CategoryTheory.InducedCategory.Hom.hom 0) = 0

The zero morphism has the zero complex linear map underneath.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.add_toLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f g : X ⟶ Y) : MixedHodgeStructure.Hom.toLinearMap (f + g).hom = MixedHodgeStructure.Hom.toLinearMap f.hom + MixedHodgeStructure.Hom.toLinearMap g.hom

Addition of morphisms is addition of their underlying complex linear maps.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.smul_toLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (q : ℚ) (f : X ⟶ Y) : MixedHodgeStructure.Hom.toLinearMap (q • f).hom = ↑q • MixedHodgeStructure.Hom.toLinearMap f.hom

Rational scalar multiplication passes to the underlying complex linear map.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.mixed {n : ℤ} : CategoryTheory.Functor (PolarizableHodgeStructureCat n) MixedHodgeStructureCat

Regard a polarizable pure Hodge structure as a mixed Hodge structure concentrated in its weight.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.mixed_obj {n : ℤ} (X : PolarizableHodgeStructureCat n) : mixed.obj X = X.asMixed

The mixed realization sends an object to its concentrated mixed Hodge structure.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.mixed_map_hom {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : mixed.map f ≍ f.hom

The mixed realization sends a morphism to its underlying mixed-Hodge morphism, up to the object equalities in mixed_obj.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.mixed_map {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : mixed.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.eqToHom ⋯))

The morphism formula for the mixed realization, with its source and target transported along mixed_obj.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instFullMixedHodgeStructureCatMixed {n : ℤ} : mixed.Full

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instFaithfulMixedHodgeStructureCatMixed {n : ℤ} : mixed.Faithful

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instAdditiveMixedHodgeStructureCatMixed {n : ℤ} : mixed.Additive

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instLinearRatMixedHodgeStructureCatMixed {n : ℤ} : CategoryTheory.Functor.Linear ℚ mixed

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.rational {n : ℤ} : CategoryTheory.Functor (PolarizableHodgeStructureCat n) (ModuleCat ℚ)

The rational realization, induced from the rational realization of mixed Hodge structures.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.rational_obj {n : ℤ} (X : PolarizableHodgeStructureCat n) : rational.obj X = X.rat

The rational realization sends an object to its rational vector space.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.rational_map_hom {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : ModuleCat.Hom.hom (rational.map f) ≍ f.hom.toRatLinearMap

The rational realization sends a morphism to its underlying rational linear map, up to the object equalities in rational_obj.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.rational_map {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : rational.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom f.hom.toRatLinearMap) (CategoryTheory.eqToHom ⋯))

The morphism formula for the rational realization, with its source and target transported along rational_obj.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instFaithfulModuleCatRatRational {n : ℤ} : rational.Faithful

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instAdditiveModuleCatRatRational {n : ℤ} : rational.Additive

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instLinearRatModuleCatRational {n : ℤ} : CategoryTheory.Functor.Linear ℚ rational

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.complex {n : ℤ} : CategoryTheory.Functor (PolarizableHodgeStructureCat n) (ModuleCat ℂ)

The complex realization, induced from the complex realization of mixed Hodge structures.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.complex_obj {n : ℤ} (X : PolarizableHodgeStructureCat n) : complex.obj X = X.complexSpace

The complex realization sends an object to its complex vector space.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.complex_map_hom {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : ModuleCat.Hom.hom (complex.map f) ≍ MixedHodgeStructure.Hom.toLinearMap f.hom

The complex realization sends a morphism to its derived complex linear map, up to the object equalities in complex_obj.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.complex_map {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (f : X ⟶ Y) : complex.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (MixedHodgeStructure.Hom.toLinearMap f.hom)) (CategoryTheory.eqToHom ⋯))

The morphism formula for the complex realization, with its source and target transported along complex_obj.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instAdditiveModuleCatComplexComplex {n : ℤ} : complex.Additive

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instLinearRatModuleCatComplexComplex {n : ℤ} : CategoryTheory.Functor.Linear ℚ complex

The complex realization is rational-linear through the inclusion ℚ → ℂ.