Positive planes in a real quadratic space of signature (2, n - 2)

A quadratic space (M, Q) over ℝ whose signature is (2, n - 2) carries a distinguished family of two-dimensional subspaces: the positive planes, the planes on which Q is positive definite. This file owns that neutral carrier; OrthogonalityLocus.lean separately owns the loci cut out inside it.

In the K3 application, M = N(X) ⊗ ℝ and a complex vector determines an ordered frame (Re Ω, Im Ω), which then forgets to the plane it spans. Those three presentations are not interchangeable. PositiveFrame.lean supplies the explicit frame-to-plane map; a geometric period-domain identification must be stated with its geometric realization.

No geometry is asserted here. Every statement below is a statement about an arbitrary real quadratic space of signature (2, n - 2) and is true whether or not any K3 surface exists; the identification of such a space with N(X) ⊗ ℝ needs Dᵇ(Coh X), Chern characters and Hirzebruch–Riemann–Roch, none of which appear here. This is the discipline LinearAlgebra/Lattice/Mukai/Basic.lean states for the integral lattice, applied to its real span.

The two conventions, and which one is used

Bridgeland writes the pairing bilinearly: a spherical class has (δ, δ) = -2. Mathlib's signature API is quadratic-form-native (sigPos, sigNeg), and the bilinear form belonging to a QuadraticForm is its polar form, which satisfies polar Q δ δ = 2 * Q δ. Q carries the Sylvester theory and Q.polarBilin is the pairing; spherical-class and orthogonality-locus terminology starts in OrthogonalityLocus.lean.

Main results

• Nondegenerate of the form, from the signature hypothesis alone.
• isCompl_orthogonal — M = W ⊕ Wᗮ for a positive plane W.
• neg_of_mem_orthogonal and negDef_orthogonal — the engine: Q is negative definite on Wᗮ. Downstream orthogonality-finiteness statements rest on this, since it makes the pairing definite on the orthogonal space.
• exists_isPositivePlane and stdForm_hasSignatureTwo — the hypothesis is inhabited and its positive-plane locus is nonempty, so nothing above is vacuous. sigPos Q = 2 carries its own positive plane; stdForm is x₀² + x₁² - x₂² on ℝ³, the smallest space the hypothesis holds for.

What is deliberately absent

• Finiteness of orthogonality loci. That needs a lattice inside M and its discreteness on top of negDef_orthogonal; it is not a statement about the real quadratic space alone.
• The component P⁺ of P. Choosing the connected component containing exp(iω) is orientation data on the positive plane. Nothing below needs it.
• A complex-vector or geometric period domain. Bridgeland's domain sits in M ⊗ ℝ ℂ, while positivePlanes Q is a set of submodules. Passing through (Re Ω, Im Ω) forgets an ordered basis and then its orientation; it is a map, not a rename or a literal identification of carriers.

structure PeriodDomain.IsPositivePlane {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (W : Submodule ℝ M) : Prop

A positive plane: a two-dimensional subspace on which Q is positive definite. In the K3 case these are the planes spanned by Re Ω and Im Ω for Ω in Bridgeland's P(X).

• finrank_eq : Module.finrank ℝ ↥W = 2

  The subspace is a plane.

• posDef : (QuadraticMap.restrict Q W).PosDef

  Q is positive definite on it.

structure PeriodDomain.HasSignatureTwo {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : Prop

The signature hypothesis: (2, n - 2), written without truncated subtraction. Nondegeneracy is a consequence rather than a field, see nondegenerate.

• sigPos_eq : sigPos Q = 2

  The positive index of inertia is 2.

• sigNeg_add_two : sigNeg Q + 2 = Module.finrank ℝ M

  The negative index of inertia takes up everything else.

def PeriodDomain.positivePlanes {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : Set (Submodule ℝ M)

The locus of all positive planes.

Equations

• PeriodDomain.positivePlanes Q = {W : Submodule ℝ M | PeriodDomain.IsPositivePlane Q W}

theorem PeriodDomain.polarBilin_isRefl {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} : LinearMap.IsRefl (QuadraticMap.polarBilin Q)

The pairing is symmetric, hence reflexive.

theorem PeriodDomain.restrict_nondegenerate_of_isPositivePlane {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} (hW : IsPositivePlane Q W) : (LinearMap.BilinForm.restrict (QuadraticMap.polarBilin Q) W).Nondegenerate

The pairing is nondegenerate on a positive plane: a vector of the plane orthogonal to the whole plane is orthogonal to itself, so its square vanishes and positive definiteness kills it.

theorem PeriodDomain.nondegenerate {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) : QuadraticMap.Nondegenerate

The signature hypothesis leaves no radical.

theorem PeriodDomain.isCompl_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] {W : Submodule ℝ M} (hW : IsPositivePlane Q W) : IsCompl W (orthogonal Q W)

M = W ⊕ Wᗮ for a positive plane W.

theorem PeriodDomain.nonpos_of_mem_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {W : Submodule ℝ M} (hW : IsPositivePlane Q W) {u : M} (hu : u ∈ orthogonal Q W) : Q u ≤ 0

Q is nonpositive on the orthogonal complement of a positive plane. A vector of positive square there would produce a three-dimensional positive definite subspace, and sigPos Q = 2.

theorem PeriodDomain.neg_of_mem_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {W : Submodule ℝ M} (hW : IsPositivePlane Q W) {u : M} (hu : u ∈ orthogonal Q W) (hu0 : u ≠ 0) : Q u < 0

The engine. On the orthogonal complement of a positive plane the form is negative definite.

nonpos_of_mem_orthogonal gives nonpositivity; an isotropic vector there would be orthogonal to Wᗮ by polar_eq_zero_of_nonpos and to W by construction, hence to M = W ⊕ Wᗮ, hence in the radical, which the signature hypothesis makes trivial.

theorem PeriodDomain.negDef_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {W : Submodule ℝ M} (hW : IsPositivePlane Q W) : (QuadraticMap.restrict (-Q) (orthogonal Q W)).PosDef

negDef_orthogonal in the shape sigNeg consumes: -Q is positive definite on Wᗮ.

theorem PeriodDomain.finrank_orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] {W : Submodule ℝ M} (hW : IsPositivePlane Q W) : Module.finrank ℝ ↥(orthogonal Q W) + 2 = Module.finrank ℝ M

The complement of a positive plane is a hyperplane pair short of M. Only the splitting is used, so the signature hypothesis is not needed.

theorem PeriodDomain.exists_isPositivePlane {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) : ∃ (W : Submodule ℝ M), IsPositivePlane Q W

The positive-plane locus of a signature (2, n - 2) space is nonempty.

sigPos Q = 2 is exactly the assertion that a two-dimensional positive definite subspace is available, so the hypothesis carries its own witness and nothing below is vacuous.

theorem PeriodDomain.positivePlanes_nonempty {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) : (positivePlanes Q).Nonempty

noncomputable def PeriodDomain.stdForm : QuadraticForm ℝ (Fin 3 → ℝ)

The diagonal form x₀² + x₁² - x₂² on ℝ³. It is the smallest quadratic space satisfying HasSignatureTwo, and it is here so that the hypothesis is known to be inhabited rather than merely stated.

Equations

• PeriodDomain.stdForm = QuadraticMap.weightedSumSquares ℝ ![1, 1, -1]

theorem PeriodDomain.stdForm_hasSignatureTwo : HasSignatureTwo stdForm

theorem PeriodDomain.nonpos_of_sigPos_eq_one {M : Type u_1} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hsig : sigPos Q = 1) {u v : M} (hu : 0 < Q u) (horth : QuadraticMap.polar (⇑Q) u v = 0) : Q v ≤ 0

Q is nonpositive on the orthogonal complement of a positive vector when sigPos Q = 1.

The signature-one companion of nonpos_of_mem_orthogonal, which is the same statement one dimension up. A vector of positive square orthogonal to u would span, with u, a two-dimensional positive definite subspace, and sigPos Q = 1 forbids that.

With Q the intersection form of NS(X) ⊗ ℝ this is the Hodge index theorem in the form §6 consumes: c · ω = 0 and ω² > 0 give c² ≤ 0. Stated here rather than in the Mukai files because it is a fact about a real quadratic space and mentions no geometry.

Note the orthogonality hypothesis is on polar, which for a form built by toQuadraticMap is twice the underlying pairing; over ℝ that is immaterial for vanishing, but see Mukai/RealForm.lean on why the factor is not immaterial elsewhere.