Riemann forms polarize the weight-one Hodge structure of a lattice

Let V be an integral module with an almost complex structure J on its realification ℝ ⊗[ℤ] V, and let E be an integral bilinear form on V. Classically, E is a Riemann form for (V, J) when it is alternating and its real scalar extension E_ℝ satisfies the two Riemann bilinear relations

• E_ℝ (J x) (J y) = E_ℝ x y for all real x and y, and
• 0 < E_ℝ (J x) x for every nonzero real x;

that is, H (x, y) = E_ℝ (J x) y + i E_ℝ x y is a positive definite Hermitian form for the complex structure J. This is the datum of a polarized abelian variety: (ℤ^{2g}, J, E) with E a Riemann form is a complex torus ℂ^g / Λ together with a polarization.

When V is flat over ℤ, this file shows that a Riemann form is exactly an integral form polarizing the effective weight-one Hodge structure TauCeti.AlmostComplexStructure.latticeHodgeStructure that J defines on V: the Hodge–Riemann relations for that structure, whose Weil operator is the transported J, reduce to the two relations above on the real points, which are the realification. A Riemann form is also nondegenerate when V is flat over ℤ, so nondegeneracy is not part of the definition.

Sign convention: positivity is 0 < E_ℝ (J x) x, as in Birkenhake–Lange, so that the Hermitian form H above is positive definite. It matches the pinned convention of TauCeti.Hodge.IsPolarization, 0 < Q (C x) x for the Weil operator C. The symplectic compatibility predicate TauCeti.SymplecticForm.Compatible uses the opposite sign, 0 < ω x (J x), so a Riemann form is J-compatible in that sense only up to a sign.

Main declarations

• TauCeti.AlmostComplexStructure.IsRiemannForm: E is a Riemann form for J.
• TauCeti.AlmostComplexStructure.IsRiemannForm.nondegenerate: a Riemann form is nondegenerate when V is flat over ℤ.
• TauCeti.AlmostComplexStructure.IsRiemannForm.isPolarization: when V is flat over ℤ, a Riemann form polarizes the weight-one Hodge structure of J.
• TauCeti.AlmostComplexStructure.isRiemannForm_of_isPolarization: every form polarizing that Hodge structure is a Riemann form, with no flatness assumption.
• TauCeti.AlmostComplexStructure.isRiemannForm_iff_isPolarization: when V is flat over ℤ, the Riemann forms are exactly the polarizing forms.
• TauCeti.AlmostComplexStructure.IsRiemannForm.polarization: the polarized effective weight-one Hodge structure of a lattice with a complex structure and a Riemann form.
• TauCeti.Hodge.HodgeStructureOn.isRiemannForm_latticeAlmostComplexStructure_iff: read from the Hodge-structure side, when V is flat over ℤ the forms polarizing an effective weight-one Hodge structure are exactly the Riemann forms of its complex structure on the realification.

The definitions and conventions follow Birkenhake–Lange, Complex Abelian Varieties, §2.1 and §4.1, and Mumford, Abelian Varieties, §I.3; the Hodge-theoretic reading is Voisin, Hodge Theory and Complex Algebraic Geometry I, Chapter 7.

structure TauCeti.AlmostComplexStructure.IsRiemannForm {V : Type u} [AddCommGroup V] (J : AlmostComplexStructure (Hodge.Realification V)) (E : LinearMap.BilinForm ℤ V) : Prop

An integral bilinear form E on V is a Riemann form for an almost complex structure J on the realification of V when it is alternating, its real scalar extension is J-invariant, and E_ℝ (J x) x is positive for every nonzero real vector x.

Nondegeneracy follows when V is flat over ℤ (IsRiemannForm.nondegenerate), so it is not part of this definition.

• isAlt : E.IsAlt

  The form is alternating.

• invariant (x y : Hodge.Realification V) : ((LinearMap.BilinForm.baseChange ℝ E) (J.toLinearMap x)) (J.toLinearMap y) = ((LinearMap.BilinForm.baseChange ℝ E) x) y

  The first Riemann bilinear relation: the real scalar extension is J-invariant.

• positive (x : Hodge.Realification V) : x ≠ 0 → 0 < ((LinearMap.BilinForm.baseChange ℝ E) (J.toLinearMap x)) x

  The second Riemann bilinear relation: E_ℝ (J x) x is positive on nonzero real vectors.

theorem TauCeti.AlmostComplexStructure.IsRiemannForm.nondegenerate {V : Type u} [AddCommGroup V] {J : AlmostComplexStructure (Hodge.Realification V)} {E : LinearMap.BilinForm ℤ V} [Module.Flat ℤ V] (h : J.IsRiemannForm E) : E.Nondegenerate

A Riemann form is nondegenerate, on a flat (for instance free) integral module: the positivity of E_ℝ (J x) x leaves no room for a radical.

theorem TauCeti.AlmostComplexStructure.IsRiemannForm.isPolarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {J : AlmostComplexStructure (Hodge.Realification V)} {E : LinearMap.BilinForm ℤ V} [Module.Flat ℤ V] (h : J.IsRiemannForm E) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.IsPolarization hℂ (J.latticeHodgeStructure hℂ) E

A Riemann form on a flat integral module polarizes the weight-one Hodge structure of its complex structure. For the effective weight-one structure J.latticeHodgeStructure hℂ, whose Weil operator is J, the Hodge–Riemann relations of E are exactly the two Riemann bilinear relations.

def TauCeti.AlmostComplexStructure.IsRiemannForm.polarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {J : AlmostComplexStructure (Hodge.Realification V)} {E : LinearMap.BilinForm ℤ V} [Module.Flat ℤ V] (h : J.IsRiemannForm E) (hℂ : IsBaseChange ℂ ιℂ) : Hodge.Polarization hℂ (J.latticeHodgeStructure hℂ)

The polarized effective weight-one Hodge structure of a flat integral module with a complex structure and a Riemann form: the Riemann form, bundled with its Hodge–Riemann relations.

@[simp]

theorem TauCeti.AlmostComplexStructure.IsRiemannForm.polarization_Qint {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {J : AlmostComplexStructure (Hodge.Realification V)} {E : LinearMap.BilinForm ℤ V} [Module.Flat ℤ V] (h : J.IsRiemannForm E) (hℂ : IsBaseChange ℂ ιℂ) : (h.polarization hℂ).Qint = E

The integral form of the polarization defined by a Riemann form is that form.

@[simp]

theorem TauCeti.AlmostComplexStructure.IsRiemannForm.polarization_Q {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {J : AlmostComplexStructure (Hodge.Realification V)} {E : LinearMap.BilinForm ℤ V} [Module.Flat ℤ V] (h : J.IsRiemannForm E) (hℂ : IsBaseChange ℂ ιℂ) : (h.polarization hℂ).Q = hℂ.bilinForm E

The complex form of the polarization defined by a Riemann form is the complexification of that form.

theorem TauCeti.AlmostComplexStructure.isRiemannForm_of_isPolarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {J : AlmostComplexStructure (Hodge.Realification V)} {hℂ : IsBaseChange ℂ ιℂ} {E : LinearMap.BilinForm ℤ V} (h : Hodge.IsPolarization hℂ (J.latticeHodgeStructure hℂ) E) : J.IsRiemannForm E

Every form polarizing the weight-one Hodge structure of J is a Riemann form for J, with no flatness assumption: J-invariance of E_ℝ says that the Weil operator is an isometry of the polarization, and positivity of E_ℝ (J x) x is positivity of the Hodge form on real vectors.

theorem TauCeti.AlmostComplexStructure.isRiemannForm_iff_isPolarization {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} [Module.Flat ℤ V] (J : AlmostComplexStructure (Hodge.Realification V)) (hℂ : IsBaseChange ℂ ιℂ) (E : LinearMap.BilinForm ℤ V) : J.IsRiemannForm E ↔ Hodge.IsPolarization hℂ (J.latticeHodgeStructure hℂ) E

When V is flat over ℤ, the Riemann forms for J are exactly the forms polarizing its weight-one Hodge structure. Flatness is used only in the forward direction, for nondegeneracy.

theorem TauCeti.Hodge.HodgeStructureOn.isRiemannForm_latticeAlmostComplexStructure_iff {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {hℂ : IsBaseChange ℂ ιℂ} [Module.Flat ℤ V] (hs : HodgeStructure hℂ 1) (h : IsEffective hs) (E : LinearMap.BilinForm ℤ V) : (latticeAlmostComplexStructure hs ⋯).IsRiemannForm E ↔ IsPolarization hℂ hs E

When V is flat over ℤ, the forms polarizing an effective weight-one Hodge structure are exactly the Riemann forms of its complex structure on the realification. This is TauCeti.AlmostComplexStructure.isRiemannForm_iff_isPolarization read through the round trip TauCeti.AlmostComplexStructure.latticeHodgeStructureEquiv: polarized effective weight-one Hodge structures on a lattice are the data (Λ, J, E) of a polarized abelian variety.