The category of mixed Hodge structures

This file bundles mixed Hodge structures whose integral, rational, and complex carriers lie in a fixed universe. Morphisms are the rational maps from TauCeti.Hodge.MixedHodgeStructure.Hom; their complex actions remain derived by base change.

The resulting category is preadditive and ℚ-linear. The rational realization is a faithful ℚ-linear functor to ModuleCat ℚ, while the complex realization is a ℚ-linear functor to ModuleCat ℂ. These structures are the categorical input for packaging strictness as kernels and cokernels in the category of mixed Hodge structures.

Main declarations

• TauCeti.Hodge.MixedHodgeStructureCat: a bundled mixed Hodge structure.
• TauCeti.Hodge.MixedHodgeStructureCat.rational: the faithful rational realization functor.
• TauCeti.Hodge.MixedHodgeStructureCat.complex: the complex realization functor.

References

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

structure TauCeti.Hodge.MixedHodgeStructureCat : Type (u + 1)

The category of mixed Hodge structures with integral, rational, and complex carriers in Type u.

The three carrier types and the two base-change witnesses are bundled so that objects may have different underlying integral carriers. A morphism is still a single rational map: the integral carrier is the arithmetic source of the base-change models, not an extra component of a morphism.

No finiteness is imposed on the carriers. Deligne's mixed Hodge structures (Théorie de Hodge II, 2.3.1) have a finitely generated integral carrier, with morphisms defined over ℤ, and his rational ones (2.3.8) a finite-dimensional rational carrier. This category has objects his have not, and, its morphisms being rational maps, more morphisms between integral structures; the abelian structure (TauCeti.Hodge.MixedHodgeStructureCat.abelian) is that of this larger category.

• intCarrier : Type u

  The integral carrier underlying a mixed Hodge structure.

• ratCarrier : Type u

  The rational vector space underlying a mixed Hodge structure.

• complexCarrier : Type u

  The complex vector space underlying a mixed Hodge structure.

• intAddCommGroup : AddCommGroup self.intCarrier

  The additive group structure on the integral carrier.

• ratAddCommGroup : AddCommGroup self.ratCarrier

  The additive group structure on the rational vector space.

• ratModule : Module ℚ self.ratCarrier

  The rational module structure.

• complexAddCommGroup : AddCommGroup self.complexCarrier

  The additive group structure on the complex vector space.

• complexModule : Module ℂ self.complexCarrier

  The complex module structure.

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

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

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

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

• isBaseChangeRat : IsBaseChange ℚ self.toRat

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

• isBaseChangeComplex : IsBaseChange ℂ self.toComplex

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

• hs : MixedHodgeStructure ⋯ ⋯

  The mixed Hodge structure on the bundled base-change models.

@[reducible, inline]

abbrev TauCeti.Hodge.MixedHodgeStructureCat.of {Vℤ Vℚ Vℂ : Type u} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (X : MixedHodgeStructure hℚ hℂ) : MixedHodgeStructureCat

Bundle an existing mixed Hodge structure as an object of MixedHodgeStructureCat.

@[reducible, inline]

abbrev TauCeti.Hodge.MixedHodgeStructureCat.rat (X : MixedHodgeStructureCat) : ModuleCat ℚ

The rational vector space underlying a bundled mixed Hodge structure.

@[reducible, inline]

abbrev TauCeti.Hodge.MixedHodgeStructureCat.complexSpace (X : MixedHodgeStructureCat) : ModuleCat ℂ

The complex vector space underlying a bundled mixed Hodge structure.

@[instance_reducible]

noncomputable instance TauCeti.Hodge.MixedHodgeStructureCat.instCategory : CategoryTheory.Category.{u, u + 1} MixedHodgeStructureCat

theorem TauCeti.Hodge.MixedHodgeStructureCat.hom_ext {X Y : MixedHodgeStructureCat} {f g : X ⟶ Y} (h : f.toRatLinearMap = g.toRatLinearMap) : f = g

Two categorical morphisms of mixed Hodge structures are equal if their rational maps agree.

theorem TauCeti.Hodge.MixedHodgeStructureCat.hom_ext_iff {X Y : MixedHodgeStructureCat} {f g : X ⟶ Y} : f = g ↔ f.toRatLinearMap = g.toRatLinearMap

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.id_toRatLinearMap (X : MixedHodgeStructureCat) : (CategoryTheory.CategoryStruct.id X).toRatLinearMap = LinearMap.id

The identity morphism has the identity rational linear map.

@[simp]

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

Composition of categorical morphisms is composition of their rational maps.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.id_toLinearMap (X : MixedHodgeStructureCat) : MixedHodgeStructure.Hom.toLinearMap (CategoryTheory.CategoryStruct.id X) = LinearMap.id

The identity morphism has the identity complex linear map.

@[simp]

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

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

@[instance_reducible]

noncomputable instance TauCeti.Hodge.MixedHodgeStructureCat.instPreadditive : CategoryTheory.Preadditive MixedHodgeStructureCat

@[instance_reducible]

noncomputable instance TauCeti.Hodge.MixedHodgeStructureCat.instLinearRat : CategoryTheory.Linear ℚ MixedHodgeStructureCat

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.rational : CategoryTheory.Functor MixedHodgeStructureCat (ModuleCat ℚ)

The rational realization of a mixed Hodge structure and its morphisms.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.rational_obj (X : MixedHodgeStructureCat) : rational.obj X = X.rat

The rational realization sends a mixed Hodge structure to its rational vector space.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.rational_map_hom {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : ModuleCat.Hom.hom (rational.map f) = f.toRatLinearMap

The rational realization sends a morphism to its underlying rational linear map.

instance TauCeti.Hodge.MixedHodgeStructureCat.instFaithfulModuleCatRatRational : rational.Faithful

instance TauCeti.Hodge.MixedHodgeStructureCat.instAdditiveModuleCatRatRational : rational.Additive

instance TauCeti.Hodge.MixedHodgeStructureCat.instLinearRatModuleCatRational : CategoryTheory.Functor.Linear ℚ rational

noncomputable def TauCeti.Hodge.MixedHodgeStructureCat.complex : CategoryTheory.Functor MixedHodgeStructureCat (ModuleCat ℂ)

The complex realization of a mixed Hodge structure and the complexification of its morphisms.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.complex_obj (X : MixedHodgeStructureCat) : complex.obj X = X.complexSpace

The complex realization sends a mixed Hodge structure to its complex vector space.

@[simp]

theorem TauCeti.Hodge.MixedHodgeStructureCat.complex_map_hom {X Y : MixedHodgeStructureCat} (f : X ⟶ Y) : ModuleCat.Hom.hom (complex.map f) = MixedHodgeStructure.Hom.toLinearMap f

The complex realization sends a morphism to its derived complex linear map.

instance TauCeti.Hodge.MixedHodgeStructureCat.instAdditiveModuleCatComplexComplex : complex.Additive

instance TauCeti.Hodge.MixedHodgeStructureCat.instLinearRatModuleCatComplexComplex : CategoryTheory.Functor.Linear ℚ complex

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