The Hodge form of a polarization

The second Hodge–Riemann relation says that i^(p-q) Q x (conj x) is positive on the Hodge component H^{p,q}. That expression is not defined on an inhomogeneous vector, because the scalar i^(p-q) depends on the component. Inserting the Weil operator repairs this: the Hodge form

h u v = Q (C (conj u)) v

is defined on all of the ambient complex vector space, is conjugate-linear in its first argument and linear in its second. On the diagonal of H^{p,q} it gives the classical expression i^(p-q) Q x (conj x). This file constructs it and proves that it is a positive definite Hermitian form.

The two inputs are the Weil operator's compatibilities with the polarizing form: C is an isometry of Q, and C commutes with conjugation. These compatibilities enter the Hermitian and Weil-operator invariance identities. Sesquilinearity itself comes directly from composing the complex-bilinear form with the conjugate-linear map latticeConj. Positive definiteness comes from the Hodge decomposition: distinct Hodge components are h-orthogonal, so h x x is the sum of the positive contributions of the components of x.

Conventions

Following Mathlib's LinearMap.IsSymm, the Hodge form is taken conjugate-linear in the first argument and linear in the second, whereas Hodge theory usually writes Q (C u) (conj v), which is conjugate-linear in the second. The two conventions are exchanged by conjugating, which is TauCeti.Hodge.Polarization.hodgeForm_eq_conj; the choice made here is the one for which Mathlib's IsSymm, IsNonneg and IsPosSemidef are stated. The sign conventions for the form itself are those pinned in TauCeti.Hodge.IsPolarization.

Main declarations

• TauCeti.Hodge.HodgeStructureOn.apply_weilOperator_conj_self_of_mem_piece: for any complex form with the weight symmetry of a polarization, B (C (conj x)) x = i^(p-q) B x (conj x) on H^{p,q}; this is the value of the Hodge form on a Hodge component.
• TauCeti.Hodge.Polarization.hodgeForm: the Hodge form of a polarization.
• TauCeti.Hodge.Polarization.hodgeForm_eq_conj: it is the conjugate of the alternate-convention whole-space form Q (C u) (conj v).
• TauCeti.Hodge.Polarization.isSymm_hodgeForm: it is Hermitian.
• TauCeti.Hodge.Polarization.hodgeForm_eq_zero_of_mem_piece: distinct Hodge components are orthogonal for it.
• TauCeti.Hodge.Polarization.hodgeForm_self_pos: it is positive definite.
• TauCeti.Hodge.IsPolarization.bilinForm_weilOperator_self_pos: read on the diagonal at a real vector, positive definiteness says that a polarizing form is positive on (C v, v).
• TauCeti.Hodge.Polarization.isPosSemidef_hodgeForm and TauCeti.Hodge.Polarization.hodgeForm_nondegenerate: the packaged consequences.
• TauCeti.Hodge.tate_hodgeForm_apply: the Hodge form of the polarized Tate structure ℤ(m) is the standard Hermitian form of the complex line.
• TauCeti.Hodge.IsPolarization.comp: positive definiteness makes a polarizing form pull back to a polarizing form along an injective morphism of Hodge structures.

This is the Hermitian carrier targeted in Layer L1 of TauCetiRoadmap/HodgeStructures/README.md, the form through which the polarization is used in Voisin, Hodge Theory and Complex Algebraic Geometry I, §7.1.2, and Peters–Steenbrink, Mixed Hodge Structures, §2.

Sign and power-of-i bookkeeping

theorem TauCeti.Hodge.HodgeStructureOn.apply_weilOperator_conj_self_of_mem_piece {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ω : Conjugation W} {n : ℤ} (hs : HodgeStructureOn W ω n) (B : LinearMap.BilinForm ℂ W) (hB : ∀ (x y : W), (B y) x = ↑↑n.negOnePow * (B x) y) {p : ℤ} {x : W} (hx : x ∈ hs.piece p) : (B (hs.weilOperator (ω.toEquiv x))) x = Complex.I ^ (2 * p - n) * (B x) (ω.toEquiv x)

For a complex bilinear form B with the weight symmetry B y x = (-1)^n B x y of a polarization, pairing the Weil operator of the conjugate of a vector x of the Hodge component H^{p,q} with x gives the expression i^(p-q) B x (conj x) of the second Hodge–Riemann relation.

The Hodge form

noncomputable def TauCeti.Hodge.Polarization.hodgeForm {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) : Vℂ →ₗ⋆[ℂ] Vℂ →ₗ[ℂ] ℂ

The Hodge form of a polarization: the sesquilinear form h u v = Q (C (conj u)) v, conjugate-linear in its first argument and linear in its second. For x in H^{p,q}, conjugation moves x to H^{q,p}; the action of C there, together with the weight symmetry of Q, gives h x x = i^(p-q) Q x (conj x), whose positivity is the second Hodge–Riemann relation.

theorem TauCeti.Hodge.Polarization.hodgeForm_apply {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) (u v : Vℂ) : (P.hodgeForm u) v = (P.Q ((HodgeStructureOn.weilOperator hs) ((latticeConj hℂ) u))) v

The value of the Hodge form, in terms of the complex form of the polarization.

theorem TauCeti.Hodge.Polarization.hodgeForm_eq_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) (u v : Vℂ) : (P.hodgeForm u) v = (starRingEnd ℂ) ((P.Q ((HodgeStructureOn.weilOperator hs) u)) ((latticeConj hℂ) v))

The Hodge form is the conjugate of the alternate-convention whole-space form Q (C u) (conj v). For homogeneous u ∈ H^{p,q}, the latter becomes i^(p-q) Q u (conj v).

theorem TauCeti.Hodge.Polarization.isSymm_hodgeForm {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.hodgeForm.IsSymm

The Hodge form is Hermitian.

@[simp]

theorem TauCeti.Hodge.Polarization.hodgeForm_latticeConj {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) (u v : Vℂ) : (P.hodgeForm ((latticeConj hℂ) u)) ((latticeConj hℂ) v) = (starRingEnd ℂ) ((P.hodgeForm u) v)

Conjugating both arguments of the Hodge form conjugates its value.

@[simp]

theorem TauCeti.Hodge.Polarization.hodgeForm_weilOperator {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) (u v : Vℂ) : (P.hodgeForm ((HodgeStructureOn.weilOperator hs) u)) ((HodgeStructureOn.weilOperator hs) v) = (P.hodgeForm u) v

The Weil operator is unitary for the Hodge form.

Positive definiteness

theorem TauCeti.Hodge.Polarization.hodgeForm_self_of_mem_piece {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) : (P.hodgeForm x) x = Complex.I ^ (2 * p - n) * (P.Q x) ((latticeConj hℂ) x)

On the Hodge component H^{p,q} the Hodge form is the expression i^(p-q) Q x (conj x) of the second Hodge–Riemann relation.

theorem TauCeti.Hodge.Polarization.hodgeForm_pos_of_mem_piece {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 < (P.hodgeForm x) x

The Hodge form is positive on every nonzero vector of a Hodge component.

theorem TauCeti.Hodge.Polarization.hodgeForm_eq_zero_of_mem_piece {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 p' : ℤ} (hpp : p ≠ p') {x y : Vℂ} (hx : x ∈ HodgeStructureOn.piece hs p) (hy : y ∈ HodgeStructureOn.piece hs p') : (P.hodgeForm x) y = 0

Distinct Hodge components are orthogonal for the Hodge form. Conjugation carries the p-th component to the (n-p)-th and the Weil operator preserves it, so the pairing is the pairing of the (n-p)-th and p'-th components under Q.

theorem TauCeti.Hodge.Polarization.hodgeForm_self_pos {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 : Vℂ} (hx : x ≠ 0) : 0 < (P.hodgeForm x) x

The Hodge form is positive definite. Expanding a nonzero vector into its Hodge components and using their orthogonality, the value on the diagonal is a sum of positive contributions, one for each nonzero component.

theorem TauCeti.Hodge.Polarization.hodgeForm_self_nonneg {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 : Vℂ) : 0 ≤ (P.hodgeForm x) x

The Hodge form is nonnegative on the diagonal.

theorem TauCeti.Hodge.Polarization.isNonneg_hodgeForm {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.hodgeForm.IsNonneg

The Hodge form is nonnegative, in Mathlib's packaging.

theorem TauCeti.Hodge.Polarization.isPosSemidef_hodgeForm {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.hodgeForm.IsPosSemidef

The Hodge form is positive semidefinite, in Mathlib's packaging.

@[simp]

theorem TauCeti.Hodge.Polarization.hodgeForm_self_eq_zero_iff {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 : Vℂ} : (P.hodgeForm x) x = 0 ↔ x = 0

The Hodge form vanishes on the diagonal only at zero.

theorem TauCeti.Hodge.Polarization.hodgeForm_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.hodgeForm.Nondegenerate

A positive definite form is nondegenerate: a vector orthogonal to everything is orthogonal to itself.

theorem TauCeti.Hodge.IsPolarization.bilinForm_weilOperator_self_pos {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) {v : Vℂ} (hv : v ∈ realPoints (latticeConj hℂ)) (hv0 : v ≠ 0) : 0 < ((hℂ.bilinForm Q) ((HodgeStructureOn.weilOperator hs) v)) v

A polarizing form is positive on (C v, v) for every nonzero real vector v. This is the Hodge form of the polarization evaluated on the diagonal, where the conjugation in its first argument acts trivially. In weight one it is the second Riemann bilinear relation.

@[simp]

theorem TauCeti.Hodge.tate_hodgeForm_apply (m : ℤ) (x y : ℂ) : ((tatePolarization m).hodgeForm x) y = (starRingEnd ℂ) x * y

The Hodge form of the polarized Tate structure ℤ(m) is the standard Hermitian form of the complex line: its Weil operator is the identity and its conjugation is complex conjugation.

Pulling back a polarization along an injective morphism

theorem TauCeti.Hodge.IsPolarization.comp {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {hs' : HodgeStructure h'ℂ n} {Q : LinearMap.BilinForm ℤ V} (hQ : IsPolarization hℂ hs Q) (f : hs'.Hom hs) (hf : Function.Injective ⇑f.toIntLinearMap) : IsPolarization h'ℂ hs' (Q.comp f.toIntLinearMap f.toIntLinearMap)

Polarizations pull back along injective morphisms. If Q polarizes hs and f is an injective morphism into hs from a Hodge structure of the same weight, then the form Q (f x) (f y) polarizes the source. Nondegeneracy of the pulled-back form is a consequence of the positivity of the Hodge form of Q.

theorem TauCeti.Hodge.IsPolarizable.of_injective {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} {n : ℤ} {hs : HodgeStructure hℂ n} {V' : Type u_1} {V'ℂ : Type u_2} [AddCommGroup V'] [AddCommGroup V'ℂ] [Module ℂ V'ℂ] {ι'ℂ : V' →ₗ[ℤ] V'ℂ} {h'ℂ : IsBaseChange ℂ ι'ℂ} {hs' : HodgeStructure h'ℂ n} (h : IsPolarizable hℂ hs) (f : hs'.Hom hs) (hf : Function.Injective ⇑f.toIntLinearMap) : IsPolarizable h'ℂ hs'

A Hodge structure admitting an injective morphism into a polarizable Hodge structure of the same weight is polarizable.