Polarizable pure Hodge structures are semisimple

A polarization splits off every rational Hodge substructure, so the lattice of rational Hodge substructures of a polarizable pure Hodge structure is complemented. Over a finite-dimensional rational space that lattice is also modular and satisfies the descending chain condition, and the two properties together give the classical decomposition: a polarizable pure Hodge structure is the direct sum of finitely many simple rational Hodge substructures — the atoms of the lattice — independent and spanning.

The complement itself is the orthogonal complement TauCeti.Hodge.RationalHodgeSubstructure.orthogonal for a polarizing form; the decomposition is then the lattice-theoretic TauCeti.exists_finset_isAtom_sup_eq, which splits off one atom at a time in any complemented modular lattice with the descending chain condition. Only some polarizing form is used, never a chosen one, so the statements are about TauCeti.Hodge.IsPolarizable structures: this is the semisimplicity of the polarizable Hodge structures, for which the choice of a form is not part of the object. Categorically, every monomorphism of polarizable rational Hodge structures corestricts to an isomorphism onto its rational image. The orthogonal retraction of that image therefore splits the original monomorphism, making TauCeti.Hodge.PolarizableHodgeStructureCat a SplitMonoCategory. The finite independent family of atoms also assembles through categorical biproducts, so every object is isomorphic to a finite biproduct of simple objects.

Following Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2.

Main declarations

• TauCeti.Hodge.RationalHodgeSubstructure.complementedLattice_of_isPolarizable: the lattice of rational Hodge substructures of a polarizable pure Hodge structure is complemented.
• TauCeti.Hodge.RationalHodgeSubstructure.exists_finset_isAtom_sup_eq: every rational Hodge substructure is the supremum of a finite independent family of simple substructures.
• TauCeti.Hodge.exists_finset_isAtom_sup_eq_top: semisimplicity, a polarizable pure Hodge structure is the direct sum of finitely many simple rational Hodge substructures.
• TauCeti.Hodge.PolarizableHodgeStructureCat.instSplitMonoCategory: every monomorphism of polarizable rational Hodge structures splits.
• TauCeti.Hodge.PolarizableHodgeStructureCat.exists_iso_biproduct_simple: every object is isomorphic to a finite biproduct of simple objects.

theorem TauCeti.Hodge.RationalHodgeSubstructure.complementedLattice {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} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) : ComplementedLattice (RationalHodgeSubstructure hℚ hs)

A polarization makes the lattice of rational Hodge substructures complemented: the orthogonal complement for its form is a lattice complement.

theorem TauCeti.Hodge.RationalHodgeSubstructure.complementedLattice_of_isPolarizable {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} [Module.Finite ℚ Vℚ] (h : IsPolarizable hℂ hs) : ComplementedLattice (RationalHodgeSubstructure hℚ hs)

Every rational Hodge substructure of a polarizable pure Hodge structure is a direct summand: the lattice of rational Hodge substructures is complemented.

theorem TauCeti.Hodge.RationalHodgeSubstructure.exists_finset_isAtom_sup_eq {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} [Module.Finite ℚ Vℚ] (P : Polarization hℂ hs) (W : RationalHodgeSubstructure hℚ hs) : ∃ (s : Finset (RationalHodgeSubstructure hℚ hs)), (∀ U ∈ s, IsAtom U) ∧ s.SupIndep id ∧ s.sup id = W

Every rational Hodge substructure of a polarized pure Hodge structure is a finite direct sum of simple substructures: it is the supremum of a finite independent family of atoms of the lattice of rational Hodge substructures.

theorem TauCeti.Hodge.exists_finset_isAtom_sup_eq_top {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 ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} [Module.Finite ℚ Vℚ] (hℚ : IsBaseChange ℚ ιℚ) (h : IsPolarizable hℂ hs) : ∃ (s : Finset (RationalHodgeSubstructure hℚ hs)), (∀ U ∈ s, IsAtom U) ∧ s.SupIndep id ∧ s.sup id = ⊤

Semisimplicity of polarizable pure Hodge structures. A polarizable pure Hodge structure on a finite-dimensional rational space is the direct sum of finitely many simple rational Hodge substructures: there is a finite independent family of atoms of the lattice of rational Hodge substructures whose supremum is everything.

instance TauCeti.Hodge.PolarizableHodgeStructureCat.instSplitMonoCategory {n' : ℤ} : CategoryTheory.SplitMonoCategory (PolarizableHodgeStructureCat n')

Categorical semisimplicity of polarizable rational Hodge structures. Every monomorphism splits. The splitting is obtained by identifying the source with the rational image and then using the orthogonal retraction of that image in the target.

Decomposition into simple objects

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductDesc {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) : (⨁ fun (U : ↥s) => X.ofSubstructure ↑U) ⟶ X

The canonical map from the biproduct of a finite family of rational Hodge substructures to the ambient Hodge structure.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.biproduct_ι_comp_substructureBiproductDesc {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (U : ↥s) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (U : ↥s) => X.ofSubstructure ↑U) U) (X.substructureBiproductDesc s) = X.substructureInclusion ↑U

The canonical map out of the biproduct restricts on each summand to the inclusion of the corresponding rational Hodge substructure.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.biproduct_ι_comp_substructureBiproductDesc_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (U : ↥s) {Z : PolarizableHodgeStructureCat n} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (U : ↥s) => X.ofSubstructure ↑U) U) (CategoryTheory.CategoryStruct.comp (X.substructureBiproductDesc s) h) = CategoryTheory.CategoryStruct.comp (X.substructureInclusion ↑U) h

The canonical map out of the biproduct restricts on each summand to the inclusion of the corresponding rational Hodge substructure.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.surjective_of_isAtom_of_ne_zero {n : ℤ} (X : PolarizableHodgeStructureCat n) {Y : PolarizableHodgeStructureCat n} {U : RationalHodgeSubstructure ⋯ X.hs} (hU : IsAtom U) {f : Y ⟶ X.ofSubstructure U} (hf : f ≠ 0) : Function.Surjective ⇑f.hom.toRatLinearMap

A nonzero morphism into the object induced by an atomic rational Hodge substructure is surjective on rational carriers.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.simple_of_isAtom {n : ℤ} (X : PolarizableHodgeStructureCat n) {U : RationalHodgeSubstructure ⋯ X.hs} (hU : IsAtom U) : CategoryTheory.Simple (X.ofSubstructure U)

An atom of the lattice of rational Hodge substructures gives a simple object of the category of polarizable rational Hodge structures.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductLift {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : X ⟶ ⨁ fun (U : ↥s) => X.ofSubstructure ↑U

The map from the ambient object to the biproduct given by projection onto each member of an independent spanning family along the supremum of the other members.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductLift_π {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductLift s hind htop) (CategoryTheory.Limits.biproduct.π (fun (U : ↥s) => X.ofSubstructure ↑U) U) = X.substructureRetractionOfIsCompl (↑U) ((s.erase ↑U).sup id) ⋯

Each component of the lift from an independent spanning family is projection along the supremum of the other substructures.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductLift_π_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) {Z : PolarizableHodgeStructureCat n} (h : X.ofSubstructure ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductLift s hind htop) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (U : ↥s) => X.ofSubstructure ↑U) U) h) = CategoryTheory.CategoryStruct.comp (X.substructureRetractionOfIsCompl (↑U) ((s.erase ↑U).sup id) ⋯) h

Each component of the lift from an independent spanning family is projection along the supremum of the other substructures.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductDesc_comp_substructureBiproductLift {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductDesc s) (X.substructureBiproductLift s hind htop) = CategoryTheory.CategoryStruct.id (⨁ fun (U : ↥s) => X.ofSubstructure ↑U)

The canonical map out of an independent spanning biproduct followed by its projection map is the identity.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductDesc_comp_substructureBiproductLift_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) {Z : PolarizableHodgeStructureCat n} (h : (⨁ fun (U : ↥s) => X.ofSubstructure ↑U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductDesc s) (CategoryTheory.CategoryStruct.comp (X.substructureBiproductLift s hind htop) h) = h

The canonical map out of an independent spanning biproduct followed by its projection map is the identity.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.surjective_substructureBiproductDesc_toRatLinearMap {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (htop : s.sup id = ⊤) : Function.Surjective ⇑(X.substructureBiproductDesc s).hom.toRatLinearMap

The canonical map from an independent spanning biproduct is surjective on rational carriers.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.isIso_substructureBiproductDesc {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : CategoryTheory.IsIso (X.substructureBiproductDesc s)

The canonical map from an independent spanning biproduct is an isomorphism.

noncomputable def TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductIso {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : (⨁ fun (U : ↥s) => X.ofSubstructure ↑U) ≅ X

An independent finite family of rational Hodge substructures spanning the ambient structure gives an isomorphism from their biproduct to the ambient object.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductIso_hom {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : (X.substructureBiproductIso s hind htop).hom = X.substructureBiproductDesc s

The forward map of the biproduct isomorphism is the canonical map induced by the substructure inclusions.

@[simp]

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductIso_inv {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) : (X.substructureBiproductIso s hind htop).inv = X.substructureBiproductLift s hind htop

The inverse of the biproduct isomorphism is the lift of the complementary retractions.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.biproduct_ι_comp_substructureBiproductIso_hom {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (U : ↥s) => X.ofSubstructure ↑U) U) (X.substructureBiproductIso s hind htop).hom = X.substructureInclusion ↑U

The isomorphism from an independent spanning family restricts on each summand to its substructure inclusion.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.biproduct_ι_comp_substructureBiproductIso_hom_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) {Z : PolarizableHodgeStructureCat n} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (U : ↥s) => X.ofSubstructure ↑U) U) (CategoryTheory.CategoryStruct.comp (X.substructureBiproductIso s hind htop).hom h) = CategoryTheory.CategoryStruct.comp (X.substructureInclusion ↑U) h

The isomorphism from an independent spanning family restricts on each summand to its substructure inclusion.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductIso_inv_comp_biproduct_π {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductIso s hind htop).inv (CategoryTheory.Limits.biproduct.π (fun (U : ↥s) => X.ofSubstructure ↑U) U) = X.substructureRetractionOfIsCompl (↑U) ((s.erase ↑U).sup id) ⋯

Each component of the inverse of the biproduct isomorphism is projection along the supremum of the other substructures.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.substructureBiproductIso_inv_comp_biproduct_π_assoc {n : ℤ} (X : PolarizableHodgeStructureCat n) [DecidableEq (RationalHodgeSubstructure ⋯ X.hs)] (s : Finset (RationalHodgeSubstructure ⋯ X.hs)) (hind : s.SupIndep id) (htop : s.sup id = ⊤) (U : ↥s) {Z : PolarizableHodgeStructureCat n} (h : X.ofSubstructure ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.substructureBiproductIso s hind htop).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (U : ↥s) => X.ofSubstructure ↑U) U) h) = CategoryTheory.CategoryStruct.comp (X.substructureRetractionOfIsCompl (↑U) ((s.erase ↑U).sup id) ⋯) h

Each component of the inverse of the biproduct isomorphism is projection along the supremum of the other substructures.

theorem TauCeti.Hodge.PolarizableHodgeStructureCat.exists_iso_biproduct_simple {n : ℤ} (X : PolarizableHodgeStructureCat n) : ∃ (s : Finset (RationalHodgeSubstructure ⋯ X.hs)), (∀ U ∈ s, CategoryTheory.Simple (X.ofSubstructure U)) ∧ Nonempty ((⨁ fun (U : ↥s) => X.ofSubstructure ↑U) ≅ X)

Categorical semisimplicity of polarizable rational Hodge structures. Every object is isomorphic to a finite biproduct of simple objects induced by rational Hodge substructures.