Orthogonal complements of rational Hodge substructures #
A polarization of a pure Hodge structure splits off every rational Hodge substructure: the
orthogonal complement of the substructure for the rationalified polarizing form is again a rational
Hodge substructure, and the two are complementary both over ℚ and after complexification. This is
the semisimplicity statement for polarizable rational Hodge structures in the form the theory uses
it — a subobject of a polarizable Hodge structure is a direct summand.
Two facts about the polarizing form drive the argument, and neither of them needs the Hermitian
Hodge metric. First, the Hodge–Riemann orthogonality of the components says the form pairs H^{p,q}
only against H^{q,p}, so the orthogonal complement of a component-spanned subspace is again
component-spanned: TauCeti.Hodge.IsPolarization.orthogonal_le_iSup_inf_piece, proved through the
Hodge projections TauCeti.Hodge.HodgeStructureOn.proj. Second, on a component the Hodge–Riemann
positivity makes the pairing of a vector with its conjugate nonzero; since the complexification of
a rational subspace is conjugation-stable, no nonzero vector of it is orthogonal to all of it,
which is TauCeti.Hodge.IsPolarization.disjoint_orthogonal.
Rationality of the complement is not an extra hypothesis but a computation: the complexification of
the rational orthogonal complement is the complex orthogonal complement
(TauCeti.Hodge.RationalHodgeSubstructure.rationalToComplexSubmodule_orthogonal). One inclusion is
the compatibility of the two scalar extensions of the integral form; the reverse holds because both
subspaces complement the substructure, the rational one by Mathlib's
LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint applied over ℚ.
This is Layer L1 of TauCetiRoadmap/HodgeStructures/README.md, following Voisin, Hodge Theory and
Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2.
Main declarations #
TauCeti.Hodge.IsPolarization.orthogonal_le_iSup_inf_piece: the orthogonal complement of a component-spanned subspace is component-spanned.TauCeti.Hodge.IsPolarization.disjoint_orthogonal: a conjugation-stable component-spanned subspace meets its orthogonal complement trivially.TauCeti.Hodge.RationalHodgeSubstructure.orthogonal: the orthogonal complement of a rational Hodge substructure, again a rational Hodge substructure.TauCeti.Hodge.RationalHodgeSubstructure.isCompl_orthogonal: it is a complement in the lattice of rational Hodge substructures, withTauCeti.Hodge.RationalHodgeSubstructure.isCompl_WQ_orthogonal_WQandTauCeti.Hodge.RationalHodgeSubstructure.isCompl_WC_orthogonal_WCthe same statement for the rational subspace and after complexification.TauCeti.Hodge.RationalHodgeSubstructure.bilinForm_orthogonal_top_eq_bot: the rationalified polarizing form is nondegenerate.TauCeti.Hodge.exists_isCompl_of_isPolarizable: every rational Hodge substructure of a polarizable pure Hodge structure has an orthogonal direct-sum complement.
A Hodge projection of a vector orthogonal to a component-spanned subspace is again orthogonal to it: the polarizing form pairs a Hodge component only against the complementary one, so the orthogonality conditions decouple along the Hodge decomposition.
The orthogonal complement of a sub-Hodge structure is a sub-Hodge structure. The orthogonal complement of a subspace spanned by its intersections with the Hodge components is again spanned by its intersections with the Hodge components.
A polarization is nondegenerate on a sub-Hodge structure. A conjugation-stable subspace spanned by its intersections with the Hodge components meets its orthogonal complement trivially: a nonzero vector of a Hodge component pairs nontrivially with its conjugate, which conjugation stability keeps inside the subspace.
A polarization is nondegenerate on the complexification of a rational Hodge substructure.
The rationalified polarizing form is reflexive: it is symmetric or antisymmetric according to the parity of the weight.
The complexification of the rational orthogonal complement is contained in the complex orthogonal complement.
The orthogonal complement of a rational Hodge substructure is defined over ℚ: the
complexification of the rational orthogonal complement is the complex orthogonal complement. Both
subspaces complement the complexified substructure and one contains the other, so they agree.
The orthogonal complement of a rational Hodge substructure for a chosen polarization: the orthogonal complement of its rational subspace. It is again a rational Hodge substructure, because its complexification is the complex orthogonal complement, and that is spanned by its intersections with the Hodge components.
Instances For
A polarization splits a rational Hodge substructure off, over ℚ.
A polarization splits a rational Hodge substructure off in the lattice of rational Hodge substructures: the orthogonal complement is a complement there, not merely a complementary subspace.
A polarization splits a rational Hodge substructure off, after complexification.
The rationalified polarizing form is nondegenerate: only zero is orthogonal to the whole rational space.
Semisimplicity of polarizable rational Hodge structures. Every rational Hodge substructure
of a polarizable pure Hodge structure has a complement, both over ℚ and after complexification,
orthogonal to it for some polarization.