Documentation

TauCeti.Geometry.Hodge.WeightOne.Polarization

The Riemann bilinear relations in weight one #

An effective Hodge structure of weight one has only the two Hodge components H^{1,0} and H^{0,1}, and its Weil operator C restricts to a complex structure on the real form of its lattice. For such a structure the Hodge–Riemann relations become the two classical Riemann bilinear relations, which speak only about real vectors: a nondegenerate alternating integral form Q polarizes the structure as soon as

Both relations are also necessary — the first is TauCeti.Hodge.IsPolarization.isOrthogonal_weilOperator read on real vectors, and the second is TauCeti.Hodge.IsPolarization.bilinForm_weilOperator_self_pos, which holds in arbitrary weight — so among nondegenerate alternating forms the two relations characterize the polarizing ones. This is the shape in which a Riemann form on a lattice with a complex structure polarizes the weight-one Hodge structure it carries, as for the first cohomology of a complex torus.

Effectivity is what makes the two relations sufficient, and it is not decoration. The operator C acts on H^{p,1-p} by i^{2p-1}, so invariance of Q under C forces that component to be orthogonal to H^{p',1-p'} only when p and p' have the same parity. For an effective structure the sole orthogonality a polarization asks for is H^{1,0} against itself, a pair of equal — hence equal-parity — degrees. A non-effective weight-one structure also has components H^{p,1-p} with p ∉ {0, 1}, where the relations pair degrees of opposite parity, so it is not covered.

Main declarations #

The conventions are those pinned in TauCeti.Hodge.IsPolarization; the relations follow Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2.

theorem TauCeti.Hodge.isPolarization_of_weilOperator_invariant_on_realPoints_of_pos {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {Q : LinearMap.BilinForm ℤ V} {hs : HodgeStructure hℂ 1} (heff : HodgeStructureOn.IsEffective hs) (hskew : ∀ (x y : V), (Q y) x = -(Q x) y) (hnd : Q.Nondegenerate) (hinv : ∀ x ∈ realPoints (latticeConj hℂ), ∀ y ∈ realPoints (latticeConj hℂ), ((hℂ.bilinForm Q) ((HodgeStructureOn.weilOperator hs) x)) ((HodgeStructureOn.weilOperator hs) y) = ((hℂ.bilinForm Q) x) y) (hpos : ∀ x ∈ realPoints (latticeConj hℂ), x ≠ 0 → 0 < ((hℂ.bilinForm Q) ((HodgeStructureOn.weilOperator hs) x)) x) :
IsPolarization hℂ hs Q

The Riemann bilinear relations polarize an effective weight-one Hodge structure. Let Q be a nondegenerate antisymmetric form on the lattice of an effective Hodge structure of weight one, and let C be its Weil operator, a complex structure on the real form. If the complexification of Q is invariant under C on real vectors, and is positive on the pair (C x, x) for every nonzero real vector x, then Q polarizes the structure.

Invariance under C gives the first Hodge–Riemann relation: on H^{1,0} the operator C acts by i, so invariance forces the form to vanish there, and in weight one that is the only relation to check. Positivity on the real form gives the second: a nonzero class of H^{1,0} and its conjugate add up to a nonzero real vector on which the hypothesis applies.