Z(β,ω) on the Mukai extension

The central charge of the exponential pair, written out. For v = (r, c, s):

Z (r, c, s) = (b β c - s - r * (b β β - b ω ω) / 2) + i * (b ω c - r * b β ω)

which is Bridgeland's Z(β,ω) — his ⟪exp(β + iω), v⟫, with the pairing read on the real and imaginary parts rather than on a complexified space.

The classes of vanishing charge are exactly the orthogonal complement of the exponential plane, where the form is negative definite under the signature hypothesis. Interpreting that fact as one half of a support condition, or as a wall statement, belongs to downstream stability modules.

V is an arbitrary real bilinear space; no geometry is asserted, and v(E) for an object E is not defined here.

Why this path

This file used to sit in LinearAlgebra/Lattice/Mukai/, which put a central charge inside the quadratic extension it is computed on and let geometry consume a stability construction without declaring the edge. expCharge is PeriodDomain.centralCharge -- the neutral paired functional of QuadraticForm/ComplexPairing.lean, unchanged -- specialised at realForm and at the exponential frame, so it is an application adapter and belongs with the numerical central-charge construction. neg_of_expCharge_eq_zero and expCharge_ne_zero_of_nonneg are the comparison half: the charge kernel against the sign of realForm. They remain the kernel statement only; Weak/Support/Predicate/Quadratic.lean still owns the full support criterion.

noncomputable def Mukai.expCharge {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v : RealExtension V) : ℂ

Z(β,ω): the central charge of the exponential pair.

Equations

• Mukai.expCharge b β ω v = PeriodDomain.centralCharge (Mukai.realForm b) (Mukai.expRe b β ω) (Mukai.expIm b β ω) v

noncomputable def Mukai.expChargeHom {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : RealExtension V →+ ℂ

Z(β,ω) as an additive homomorphism.

The exponential charge is linear in the Mukai class. Exposing that structure at the numerical layer lets categorical consumers compose class maps with the charge instead of rebuilding its additivity object by object.

Equations

• Mukai.expChargeHom b β ω = { toFun := Mukai.expCharge b β ω, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Mukai.expChargeHom_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v : RealExtension V) : (expChargeHom b β ω) v = expCharge b β ω v

noncomputable def Mukai.expChargeLinearMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : RealExtension V →ₗ[ℝ] ℂ

Z(β,ω) as an ℝ-linear map.

The additive homomorphism above is enough for the wall arithmetic, but the quadratic compatibility predicates downstream are stated for an ℝ-linear charge. Real homogeneity comes from PeriodDomain.centralCharge_smul; nothing new is computed.

Equations

• Mukai.expChargeLinearMap b β ω = { toFun := Mukai.expCharge b β ω, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Mukai.expChargeLinearMap_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v : RealExtension V) : (expChargeLinearMap b β ω) v = expCharge b β ω v

theorem Mukai.expCharge_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (r : ℝ) (c : V) (s : ℝ) : expCharge b β ω (r, c, s) = ↑((b β) c - s - r * ((b β) β - (b ω) ω) / 2) + ↑((b ω) c - r * (b β) ω) * Complex.I

The charge written out on a triple. This is Bridgeland's formula.

theorem Mukai.neg_of_expCharge_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) [FiniteDimensional ℝ V] (hsig : PeriodDomain.HasSignatureTwo (realForm b)) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) {v : RealExtension V} (hv : expCharge b β ω v = 0) (hv0 : v ≠ 0) : (realForm b) v < 0

A nonzero class of vanishing charge has negative square. This is the kernel half of a quadratic support criterion, not the full support property.

theorem Mukai.expCharge_ne_zero_of_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) [FiniteDimensional ℝ V] (hsig : PeriodDomain.HasSignatureTwo (realForm b)) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) {v : RealExtension V} (hv : 0 ≤ (realForm b) v) (hv0 : v ≠ 0) : expCharge b β ω v ≠ 0

No nonzero class of nonnegative square is killed by Z(β,ω).

The elementary charge identities are projections of expChargeHom.

@[simp]

theorem Mukai.expCharge_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : expCharge b β ω 0 = 0

The exponential charge kills the zero class.

theorem Mukai.expCharge_add {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v w : RealExtension V) : expCharge b β ω (v + w) = expCharge b β ω v + expCharge b β ω w

The exponential charge is additive in the Mukai class.

theorem Mukai.expCharge_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (v : RealExtension V) : expCharge b β ω (-v) = -expCharge b β ω v

The exponential charge negates on negated classes.