The complex functional of a pair in a quadratic space

An ordered pair (x, y) — later read as the real and imaginary parts of Ω — determines

Z (v) = ⟪x, v⟫ + i ⟪y, v⟫

This is ⟪Ω, -⟫ written without complexifying the space, since ⟪·,·⟫ is the polar form. The API below is ordinary linear algebra: it packages no heart, semistable locus, support predicate, or wall arrangement.

The span, orthogonal complement, and exact kernel description are generic quadratic algebra. Signature and positive-plane consequences live in ComplexPairingSignature.lean; stability and wall interpretations live in StabilityCondition/CentralCharge/Quadratic.lean.

Main results

• centralCharge_eq_zero_iff — the kernel of Z is the orthogonal complement of the plane.

def PeriodDomain.pairSpan {M : Type u_1} [AddCommGroup M] [Module ℝ M] (x y : M) : Submodule ℝ M

The subspace spanned by an ordered pair.

Equations

• PeriodDomain.pairSpan x y = Submodule.span ℝ {x, y}

@[reducible, inline]

abbrev PeriodDomain.orthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (W : Submodule ℝ M) : Submodule ℝ M

The orthogonal complement with respect to the polar pairing.

Equations

• PeriodDomain.orthogonal Q W = LinearMap.BilinForm.orthogonal (QuadraticMap.polarBilin Q) W

theorem PeriodDomain.mem_orthogonal_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {W : Submodule ℝ M} {u : M} : u ∈ orthogonal Q W ↔ ∀ w ∈ W, QuadraticMap.polar (⇑Q) w u = 0

Membership in the orthogonal complement, written using the polar form.

theorem PeriodDomain.mem_orthogonal_span_pair_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x y u : M} : u ∈ orthogonal Q (Submodule.span ℝ {x, y}) ↔ QuadraticMap.polar (⇑Q) x u = 0 ∧ QuadraticMap.polar (⇑Q) y u = 0

Orthogonality to a span of two vectors is orthogonality to both.

def PeriodDomain.centralCharge {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x y v : M) : ℂ

The central charge of an ordered pair: the pairing against x and y read as the real and imaginary parts of a complex number.

Equations

• PeriodDomain.centralCharge Q x y v = ↑(QuadraticMap.polar (⇑Q) x v) + ↑(QuadraticMap.polar (⇑Q) y v) * Complex.I

@[simp]

theorem PeriodDomain.centralCharge_re {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y v : M) : (centralCharge Q x y v).re = QuadraticMap.polar (⇑Q) x v

@[simp]

theorem PeriodDomain.centralCharge_im {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y v : M) : (centralCharge Q x y v).im = QuadraticMap.polar (⇑Q) y v

theorem PeriodDomain.centralCharge_add {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y v w : M) : centralCharge Q x y (v + w) = centralCharge Q x y v + centralCharge Q x y w

theorem PeriodDomain.centralCharge_smul {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y v : M) (a : ℝ) : centralCharge Q x y (a • v) = ↑a * centralCharge Q x y v

@[simp]

theorem PeriodDomain.centralCharge_zero {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) : centralCharge Q x y 0 = 0

theorem PeriodDomain.centralCharge_eq_zero_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x y v : M} : centralCharge Q x y v = 0 ↔ v ∈ orthogonal Q (pairSpan x y)

The kernel of the charge is the orthogonal complement of the plane.

theorem PeriodDomain.ker_centralCharge_eq {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) : {v : M | centralCharge Q x y v = 0} = ↑(orthogonal Q (pairSpan x y))

The charge kernel as a submodule: the orthogonal complement, named for what it is in stability language.