Rational Hodge substructures as categorical retracts

A rational Hodge substructure of a polarizable pure Hodge structure is itself a polarizable object. Its rational and complex carriers are the corresponding subspaces, while its integral lattice consists of the integral vectors that land in the rational subspace.

For a chosen polarization, the inclusion of this object admits a retraction. The underlying rational map of the retraction is the orthogonal projector with codomain restricted to the substructure. Thus the composite in the ambient object is the Hodge projector, while the composite on the subobject is the identity. In particular, the inclusion is a split monomorphism.

More generally, no polarization is needed once a complement is given: a rational Hodge substructure complementary to the chosen one already determines a retraction, namely the projection onto the substructure along that complement. Its rational map is a morphism of Hodge structures because it is idempotent with a Hodge structure as range and another as kernel. This is the form used to split a substructure off an independent family, where the complement is the supremum of the other members rather than an orthogonal complement.

This is the categorical form of the orthogonal-complement argument proving semisimplicity of polarizable pure Hodge structures. See Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters--Steenbrink, Mixed Hodge Structures, §2.

Main declarations

• TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure: the polarizable object induced on a rational Hodge substructure.
• TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion: its inclusion into the ambient object.
• TauCeti.Hodge.PolarizableHodgeStructureCat.substructureLift: the factorization of a morphism through a substructure containing its rational image.
• TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetractionOfIsCompl: the retraction supplied by a complementary rational Hodge substructure.
• TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetraction: the retraction supplied by a polarization.
• TauCeti.Hodge.PolarizableHodgeStructureCat.isSplitMono_substructureInclusion: the categorical splitting.

@[implicit_reducible]

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : PolarizableHodgeStructureCat n

A rational Hodge substructure, regarded as a polarizable Hodge structure in its own right.

The integral carrier is the inverse image of the rational subspace in the ambient lattice. The rational and complex carriers are the corresponding subspaces, with the induced Hodge structure and induced polarizability.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure_intCarrier {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : (X.ofSubstructure W).intCarrier = ↥(integralSubmodule X.toRat W.WQ)

The integral carrier of the induced object consists of the integral vectors whose rational images lie in the substructure.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure_ratCarrier {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : (X.ofSubstructure W).ratCarrier = ↥W.WQ

The rational carrier of the object induced on a rational Hodge substructure is the underlying rational subspace.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure_complexCarrier {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : (X.ofSubstructure W).complexCarrier = ↥(rationalToComplexSubmodule ⋯ ⋯ W.WQ)

The complex carrier of the induced object is the complexification of its rational subspace.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.ofSubstructure_hs {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : (X.ofSubstructure W).hs = W.hodgeStructure

The pure Hodge structure on the induced object is the one obtained by restricting the ambient filtration.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : X.ofSubstructure W ⟶ X

The inclusion of an induced rational Hodge substructure into its ambient object.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : (X.substructureInclusion W).hom.toRatLinearMap = W.WQ.subtype

The rational map underlying the inclusion is the subtype map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_toLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : MixedHodgeStructure.Hom.toLinearMap (X.substructureInclusion W).hom = (rationalToComplexSubmodule ⋯ ⋯ W.WQ).subtype

The complex map underlying the inclusion is the subtype map.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isMorphism_codRestrict {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (W : RationalHodgeSubstructure ⋯ Y.hs) (f : X.ratCarrier →ₗ[ℚ] Y.ratCarrier) (hf : HodgeStructureOn.IsMorphism X.hs Y.hs (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ f)) (hfw : ∀ (x : X.ratCarrier), f x ∈ W.WQ) : HodgeStructureOn.IsMorphism X.hs W.hodgeStructure (rationalMapToComplex ⋯ ⋯ ⋯ ⋯ (LinearMap.codRestrict W.WQ f hfw))

Corestricting the rational map of a Hodge morphism to a rational Hodge substructure preserves the morphism property.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureLift {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (W : RationalHodgeSubstructure ⋯ Y.hs) (f : X ⟶ Y) (hf : ∀ (x : X.asMixed.ratCarrier), f.hom.toRatLinearMap x ∈ W.WQ) : X ⟶ Y.ofSubstructure W

A morphism whose rational image lies in a rational Hodge substructure of its target factors through that substructure.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureLift_toRatLinearMap {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (W : RationalHodgeSubstructure ⋯ Y.hs) (f : X ⟶ Y) (hf : ∀ (x : X.asMixed.ratCarrier), f.hom.toRatLinearMap x ∈ W.WQ) : (substructureLift W f hf).hom.toRatLinearMap = LinearMap.codRestrict W.WQ f.hom.toRatLinearMap hf

The rational map of the factorization through a substructure is the corestricted rational map.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureLift_comp_substructureInclusion {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (W : RationalHodgeSubstructure ⋯ Y.hs) (f : X ⟶ Y) (hf : ∀ (x : X.asMixed.ratCarrier), f.hom.toRatLinearMap x ∈ W.WQ) : CategoryTheory.CategoryStruct.comp (substructureLift W f hf) (Y.substructureInclusion W) = f

The factorization through a substructure followed by its inclusion is the original morphism.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureLift_comp_substructureInclusion_assoc {n : ℤ} {X Y : PolarizableHodgeStructureCat n} (W : RationalHodgeSubstructure ⋯ Y.hs) (f : X ⟶ Y) (hf : ∀ (x : X.asMixed.ratCarrier), f.hom.toRatLinearMap x ∈ W.WQ) {Z : PolarizableHodgeStructureCat n} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (substructureLift W f hf) (CategoryTheory.CategoryStruct.comp (Y.substructureInclusion W) h) = CategoryTheory.CategoryStruct.comp f h

The factorization through a substructure followed by its inclusion is the original morphism.

Retractions along complementary Hodge substructures

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetractionOfIsCompl {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) (h : IsCompl W W') : X ⟶ X.ofSubstructure W

The categorical retraction onto W along a complementary rational Hodge substructure W'.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetractionOfIsCompl_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) (h : IsCompl W W') : (X.substructureRetractionOfIsCompl W W' h).hom.toRatLinearMap = W.WQ.projectionOnto W'.WQ ⋯

The rational map of the retraction along a complement is the corresponding subspace projection with codomain restricted to W.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_comp_substructureRetractionOfIsCompl {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) (h : IsCompl W W') : CategoryTheory.CategoryStruct.comp (X.substructureInclusion W) (X.substructureRetractionOfIsCompl W W' h) = CategoryTheory.CategoryStruct.id (X.ofSubstructure W)

Inclusion followed by retraction along a complementary substructure is the identity.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_comp_substructureRetractionOfIsCompl_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) (h : IsCompl W W') {Z : PolarizableHodgeStructureCat n} (h✝ : X.ofSubstructure W ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.substructureInclusion W) (CategoryTheory.CategoryStruct.comp (X.substructureRetractionOfIsCompl W W' h) h✝) = h✝

Inclusion followed by retraction along a complementary substructure is the identity.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_comp_substructureRetractionOfIsCompl_eq_zero {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) {U : RationalHodgeSubstructure ⋯ X.hs} (h : IsCompl W W') (hU : U ≤ W') : CategoryTheory.CategoryStruct.comp (X.substructureInclusion U) (X.substructureRetractionOfIsCompl W W' h) = 0

A substructure contained in the complementary summand is annihilated by the retraction.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_comp_substructureRetractionOfIsCompl_eq_zero_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) {U : RationalHodgeSubstructure ⋯ X.hs} (h : IsCompl W W') (hU : U ≤ W') {Z : PolarizableHodgeStructureCat n} (h✝ : X.ofSubstructure W ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.substructureInclusion U) (CategoryTheory.CategoryStruct.comp (X.substructureRetractionOfIsCompl W W' h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

A substructure contained in the complementary summand is annihilated by the retraction.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetractionOfIsCompl_comp_substructureInclusion_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W W' : RationalHodgeSubstructure ⋯ X.hs) (h : IsCompl W W') : (CategoryTheory.CategoryStruct.comp (X.substructureRetractionOfIsCompl W W' h) (X.substructureInclusion W)).hom.toRatLinearMap = W.WQ.projection W'.WQ ⋯

Retraction along a complementary substructure followed by inclusion is the corresponding projection on the ambient rational carrier.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetraction {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) (P : Polarization ⋯ X.hs) : X ⟶ X.ofSubstructure W

The categorical retraction of a rational Hodge substructure inclusion supplied by a chosen polarization.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetraction_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) (P : Polarization ⋯ X.hs) : (X.substructureRetraction W P).hom.toRatLinearMap = W.WQ.projectionOnto (RationalHodgeSubstructure.orthogonal P W).WQ ⋯

The rational map underlying the categorical retraction is the orthogonal projector with its codomain restricted to the substructure.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureInclusion_comp_substructureRetraction {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) (P : Polarization ⋯ X.hs) : CategoryTheory.CategoryStruct.comp (X.substructureInclusion W) (X.substructureRetraction W P) = CategoryTheory.CategoryStruct.id (X.ofSubstructure W)

The inclusion followed by the orthogonal retraction is the identity on the induced Hodge structure.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureRetraction_comp_substructureInclusion_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) (P : Polarization ⋯ X.hs) : (CategoryTheory.CategoryStruct.comp (X.substructureRetraction W P) (X.substructureInclusion W)).hom.toRatLinearMap = RationalHodgeSubstructure.projection P W

The orthogonal retraction followed by the inclusion is the Hodge projector on the ambient object.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isSplitMono_substructureInclusion {n : ℤ} (X : PolarizableHodgeStructureCat n) (W : RationalHodgeSubstructure ⋯ X.hs) : CategoryTheory.IsSplitMono (X.substructureInclusion W)

The inclusion of a rational Hodge substructure into a polarizable Hodge structure is a split monomorphism.