Polarizations of pure Hodge structures

A polarization of a weight-n Hodge structure on a lattice V is an integral bilinear form on V satisfying the Hodge–Riemann bilinear relations. This file states those relations as a predicate on a fixed form, TauCeti.Hodge.IsPolarization, so that a form can be required to polarize a structure without being carried twice; bundling the form with a proof gives TauCeti.Hodge.Polarization, and forgetting the form gives the property TauCeti.Hodge.IsPolarizable.

The complex form is derived rather than postulated: it is the complexification IsBaseChange.bilinForm of the integral form, so the integral-to-complex link is a computation rather than an axiom.

Conventions

The weight sign is Q y x = (-1)^n Q x y, written with Int.negOnePow, and the positivity relation is 0 < i^(p-q) * Q x (conj x) for 0 ≠ x in the Hodge component H^{p,q}, in the partial order on ℂ available as open scoped ComplexOrder. Requiring positivity in that order also requires the value to be real, which is part of the classical statement. A geometric polarization built from a cup product carries an extra sign (-1)^(n(n-1)/2), which an instance realized that way must insert to match this convention.

Main declarations

• TauCeti.Hodge.IsPolarization: the Hodge–Riemann relations for a fixed integral form.
• TauCeti.Hodge.IsPolarization.orthogonal_piece: distinct Hodge components pair to zero unless their degrees add up to the weight.
• TauCeti.Hodge.IsPolarization.complex_nondegenerate: the complexified form of a polarization is nondegenerate.
• TauCeti.Hodge.IsPolarization.exists_pairing_ne_zero: conjugate Hodge components pair nondegenerately.
• TauCeti.Hodge.Polarization: a polarized Hodge structure's form, bundled with its relations.
• TauCeti.Hodge.IsPolarizable: existence of some polarizing form.

The Hodge–Riemann relations follow Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2. This is the definition layer of Layer L1 of TauCetiRoadmap/HodgeStructures/README.md.

structure TauCeti.Hodge.IsPolarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {n : ℤ} (hs : HodgeStructure hℂ n) (Q : LinearMap.BilinForm ℤ V) : Prop

The Hodge–Riemann bilinear relations for a fixed integral bilinear form Q on the lattice of a weight-n Hodge structure.

The form is (-1)^n-symmetric and nondegenerate; its complexification annihilates F p × F (n + 1 - p); and i^(p-q) Q x (conj x) is a positive real number for every nonzero x in the Hodge component H^{p,q}, where q = n - p.

• symm_weight (x y : V) : (Q y) x = ↑n.negOnePow * (Q x) y

  The form is symmetric in even weight and antisymmetric in odd weight.

• nondegenerate : Q.Nondegenerate

  The form has no radical.

• orthogonal (p : ℤ) (x : Vℂ) : x ∈ hs.F p → ∀ y ∈ hs.F (n + 1 - p), ((hℂ.bilinForm Q) x) y = 0

  The first Hodge–Riemann relation: F p and F (n + 1 - p) are orthogonal.

• positive (p : ℤ) (x : Vℂ) : x ∈ HodgeStructureOn.piece hs p → x ≠ 0 → 0 < Complex.I ^ (2 * p - n) * ((hℂ.bilinForm Q) x) ((latticeConj hℂ) x)

  The second Hodge–Riemann relation: i^(p-q) Q x (conj x) is positive on H^{p,q}.

theorem TauCeti.Hodge.IsPolarization.symm_of_even {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) (hn : Even n) (x y : V) : (Q y) x = (Q x) y

A polarization of an even-weight Hodge structure is a symmetric form.

theorem TauCeti.Hodge.IsPolarization.eq_neg_of_odd {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) (hn : Odd n) (x y : V) : (Q y) x = -(Q x) y

A polarization of an odd-weight Hodge structure is an antisymmetric form.

theorem TauCeti.Hodge.IsPolarization.flip_eq {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) : Q.flip = ↑n.negOnePow • Q

The flip of a polarizing form is its (-1)^n-multiple.

theorem TauCeti.Hodge.IsPolarization.complex_symm_weight {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) (x y : Vℂ) : ((hℂ.bilinForm Q) y) x = ↑↑n.negOnePow * ((hℂ.bilinForm Q) x) y

The complexification of a polarizing form obeys the same weight symmetry.

theorem TauCeti.Hodge.IsPolarization.complex_nondegenerate {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) : (hℂ.bilinForm Q).Nondegenerate

The complexification of a polarizing form is nondegenerate.

theorem TauCeti.Hodge.IsPolarization.orthogonal_conjF {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) (p : ℤ) {x y : Vℂ} (hx : x ∈ HodgeStructureOn.conjF hs p) (hy : y ∈ HodgeStructureOn.conjF hs (n + 1 - p)) : ((hℂ.bilinForm Q) x) y = 0

The first Hodge–Riemann relation transported to the conjugate filtration.

theorem TauCeti.Hodge.IsPolarization.orthogonal_piece {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) {p p' : ℤ} (hpp : p + p' ≠ n) {x y : Vℂ} (hx : x ∈ HodgeStructureOn.piece hs p) (hy : y ∈ HodgeStructureOn.piece hs p') : ((hℂ.bilinForm Q) x) y = 0

Orthogonality of the Hodge components. Two Hodge components pair to zero under a polarization unless their degrees add up to the weight.

theorem TauCeti.Hodge.IsPolarization.pairing_conj_ne_zero {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) {p : ℤ} {x : Vℂ} (hx : x ∈ HodgeStructureOn.piece hs p) (hx0 : x ≠ 0) : ((hℂ.bilinForm Q) x) ((latticeConj hℂ) x) ≠ 0

Under a polarization the Hodge–Riemann pairing of a nonzero component vector with its conjugate is nonzero.

theorem TauCeti.Hodge.IsPolarization.exists_pairing_ne_zero {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {Q : LinearMap.BilinForm ℤ V} (h : IsPolarization hℂ hs Q) {p : ℤ} {x : Vℂ} (hx : x ∈ HodgeStructureOn.piece hs p) (hx0 : x ≠ 0) : ∃ y ∈ HodgeStructureOn.piece hs (n - p), ((hℂ.bilinForm Q) x) y ≠ 0

Nondegeneracy of the Hodge–Riemann pairing between conjugate components. Every nonzero vector of H^{p,q} pairs nontrivially with a vector of H^{q,p}, namely with its conjugate.

structure TauCeti.Hodge.Polarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {n : ℤ} (hs : HodgeStructure hℂ n) : Type u

A polarization of a pure Hodge structure: an integral bilinear form on its lattice together with the Hodge–Riemann relations.

• Qint : LinearMap.BilinForm ℤ V

  The underlying integral bilinear form.

• isPolarization : IsPolarization hℂ hs self.Qint

  The Hodge–Riemann relations for that form.

noncomputable def TauCeti.Hodge.Polarization.Q {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : LinearMap.BilinForm ℂ Vℂ

The complex bilinear form of a polarization, derived by complexifying the integral form.

theorem TauCeti.Hodge.Polarization.Q_symm_weight {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (x y : Vℂ) : (P.Q y) x = ↑↑n.negOnePow * (P.Q x) y

The complex form of a polarization obeys the weight symmetry.

theorem TauCeti.Hodge.Polarization.Q_nondegenerate {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : P.Q.Nondegenerate

The complex form of a polarization is nondegenerate.

theorem TauCeti.Hodge.Polarization.Q_orthogonal {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (p : ℤ) {x y : Vℂ} (hx : x ∈ hs.F p) (hy : y ∈ hs.F (n + 1 - p)) : (P.Q x) y = 0

The complex form of a polarization satisfies the first Hodge–Riemann relation.

theorem TauCeti.Hodge.Polarization.Q_positive {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (p : ℤ) {x : Vℂ} (hx : x ∈ HodgeStructureOn.piece hs p) (hx0 : x ≠ 0) : 0 < Complex.I ^ (2 * p - n) * (P.Q x) ((latticeConj hℂ) x)

The complex form of a polarization satisfies the second Hodge–Riemann relation.

@[simp]

theorem TauCeti.Hodge.Polarization.Q_ι {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (x y : V) : (P.Q (ιℂ x)) (ιℂ y) = ↑((P.Qint x) y)

The complex form of a polarization restricts to the integral form on integral vectors.

theorem TauCeti.Hodge.Polarization.Q_def {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : P.Q = hℂ.bilinForm P.Qint

The complex bilinear form is the complexification of the integral form.

@[simp]

theorem TauCeti.Hodge.Polarization.Q_conj {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) (x y : Vℂ) : (P.Q ((latticeConj hℂ) x)) ((latticeConj hℂ) y) = (starRingEnd ℂ) ((P.Q x) y)

The complex form of a polarization takes conjugate values on conjugate arguments.

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

Two polarizations of the same Hodge structure agree as soon as their integral forms do.

theorem TauCeti.Hodge.Polarization.ext_iff {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {P P' : Polarization hℂ hs} : P = P' ↔ P.Qint = P'.Qint

def TauCeti.Hodge.IsPolarizable {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {n : ℤ} (hs : HodgeStructure hℂ n) : Prop

A pure Hodge structure is polarizable when some integral form polarizes it. This, rather than a chosen polarization, is the property under which the category of rational Hodge structures is semisimple.

theorem TauCeti.Hodge.Polarization.isPolarizable {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} (P : Polarization hℂ hs) : IsPolarizable hℂ hs

A chosen polarization exhibits a Hodge structure as polarizable.

theorem TauCeti.Hodge.isPolarizable_iff_nonempty {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} : IsPolarizable hℂ hs ↔ Nonempty (Polarization hℂ hs)

Polarizability is exactly the existence of a bundled polarization.