Direct sums of polarizable pure Hodge structures

The direct sum of two pure Hodge structures of the same weight n carries the product filtration F^p ⊕ F'^p on the product space, and its Hodge components are the products of the Hodge components. Opposedness is inherited factor by factor because a conjugation acting componentwise turns a product of subspaces into the product of their conjugates.

A polarization of the direct sum is the block-diagonal form Q ⊕ Q': the two summands are orthogonal to each other, and the Hodge–Riemann positivity of a nonzero vector (x, y) is the sum of the two contributions, of which one is positive and the other nonnegative.

Consequently the category of polarizable rational Hodge structures of weight n has binary biproducts, and with the zero object it has all finite biproducts: a finite family of polarizable Hodge structures has a direct sum which is again one. This is the ambient structure in which the decomposition of a polarizable Hodge structure into simple ones is an isomorphism onto a direct sum of objects.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.prod: the direct sum of two pure Hodge structures of the same weight, with TauCeti.Hodge.HodgeStructureOn.prod_piece describing its Hodge components.
• TauCeti.Hodge.IsPolarization.prod: the block-diagonal form polarizes the direct sum.
• TauCeti.Hodge.Polarization.prod: the direct sum of two polarizations.
• TauCeti.Hodge.IsPolarizable.prod: a direct sum of polarizable structures is polarizable.
• TauCeti.Hodge.PolarizableHodgeStructureCat.hasFiniteBiproducts: the resulting finite biproducts in the category of polarizable rational Hodge structures.

References

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

The categorical bicone construction follows TauCeti.Geometry.Hodge.Mixed.Prod.

The direct sum of two pure Hodge structures

def TauCeti.Hodge.HodgeStructureOn.prod {W : Type u} {W' : Type v} [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W'] {ω : Conjugation W} {ω' : Conjugation W'} {Ω : Conjugation (W × W')} {n : ℤ} (hs : HodgeStructureOn W ω n) (hs' : HodgeStructureOn W' ω' n) (hΩ : ∀ (x : W × W'), Ω.toEquiv x = (ω.toEquiv x.1, ω'.toEquiv x.2)) : HodgeStructureOn (W × W') Ω n

The direct sum of two Hodge structures of the same weight, filtered by the products of the two filtrations.

The conjugation Ω of the product space is required to act componentwise; for the canonical conjugation of a product of complexifications this is TauCeti.Hodge.latticeConjugation_prodMap_toEquiv_apply.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.prod_F {W : Type u} {W' : Type v} [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W'] {ω : Conjugation W} {ω' : Conjugation W'} {Ω : Conjugation (W × W')} {n : ℤ} (hs : HodgeStructureOn W ω n) (hs' : HodgeStructureOn W' ω' n) (hΩ : ∀ (x : W × W'), Ω.toEquiv x = (ω.toEquiv x.1, ω'.toEquiv x.2)) (p : ℤ) : (hs.prod hs' hΩ).F p = (hs.F p).prod (hs'.F p)

The Hodge filtration of a direct sum is the product of the two Hodge filtrations.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.prod_conjF {W : Type u} {W' : Type v} [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W'] {ω : Conjugation W} {ω' : Conjugation W'} {Ω : Conjugation (W × W')} {n : ℤ} (hs : HodgeStructureOn W ω n) (hs' : HodgeStructureOn W' ω' n) (hΩ : ∀ (x : W × W'), Ω.toEquiv x = (ω.toEquiv x.1, ω'.toEquiv x.2)) (p : ℤ) : (hs.prod hs' hΩ).conjF p = (hs.conjF p).prod (hs'.conjF p)

The conjugate filtration of a direct sum is the product of the two conjugate filtrations.

@[simp]

theorem TauCeti.Hodge.HodgeStructureOn.prod_piece {W : Type u} {W' : Type v} [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W'] {ω : Conjugation W} {ω' : Conjugation W'} {Ω : Conjugation (W × W')} {n : ℤ} (hs : HodgeStructureOn W ω n) (hs' : HodgeStructureOn W' ω' n) (hΩ : ∀ (x : W × W'), Ω.toEquiv x = (ω.toEquiv x.1, ω'.toEquiv x.2)) (p : ℤ) : (hs.prod hs' hΩ).piece p = (hs.piece p).prod (hs'.piece p)

The Hodge components of a direct sum are the products of the Hodge components.

The direct sum of two polarizations

theorem TauCeti.Hodge.IsPolarization.prod {V : Type u} {V' : Type v} {Vℂ : Type w} {V'ℂ : Type u_1} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n} {Q : LinearMap.BilinForm ℤ V} {Q' : LinearMap.BilinForm ℤ V'} (h : IsPolarization hℂ hs Q) (h' : IsPolarization h'ℂ hs' Q') : IsPolarization ⋯ (HodgeStructureOn.prod hs hs' ⋯) (Q.prod Q')

The block-diagonal form of two polarizing forms polarizes the direct sum: the summands are orthogonal to each other, so both Hodge–Riemann relations are inherited componentwise.

noncomputable def TauCeti.Hodge.Polarization.prod {V : Type u} {V' : Type v} {Vℂ : Type w} {V'ℂ : Type u_1} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') : Polarization ⋯ (HodgeStructureOn.prod hs hs' ⋯)

The direct sum of two polarizations of pure Hodge structures of the same weight.

@[simp]

theorem TauCeti.Hodge.Polarization.prod_Qint {V : Type u} {V' : Type v} {Vℂ : Type w} {V'ℂ : Type u_1} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') : (P.prod P').Qint = P.Qint.prod P'.Qint

The integral form of a direct sum of polarizations is block diagonal.

@[simp]

theorem TauCeti.Hodge.Polarization.prod_Q {V : Type u} {V' : Type v} {Vℂ : Type w} {V'ℂ : Type u_1} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n} (P : Polarization hℂ hs) (P' : Polarization h'ℂ hs') : (P.prod P').Q = P.Q.prod P'.Q

The complex form of a direct sum of polarizations is block diagonal.

theorem TauCeti.Hodge.IsPolarizable.prod {V : Type u} {V' : Type v} {Vℂ : Type w} {V'ℂ : Type u_1} [AddCommGroup V] [AddCommGroup V'] [AddCommGroup Vℂ] [Module ℂ Vℂ] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {hℂ : IsBaseChange ℂ ιℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {hs' : HodgeStructure h'ℂ n} (h : IsPolarizable hℂ hs) (h' : IsPolarizable h'ℂ hs') : IsPolarizable ⋯ (HodgeStructureOn.prod hs hs' ⋯)

A direct sum of polarizable pure Hodge structures is polarizable.

Finite biproducts in the category of polarizable Hodge structures

instance TauCeti.Hodge.PolarizableHodgeStructureCat.hasBinaryBiproducts {n : ℤ} : CategoryTheory.Limits.HasBinaryBiproducts (PolarizableHodgeStructureCat n)

instance TauCeti.Hodge.PolarizableHodgeStructureCat.hasFiniteBiproducts {n : ℤ} : CategoryTheory.Limits.HasFiniteBiproducts (PolarizableHodgeStructureCat n)

A finite family of polarizable rational Hodge structures of weight n has a direct sum, which is again a polarizable rational Hodge structure of weight n.