Z(β,ω) as a function of a numerical class #
Route (A) states the central charge on a lattice vector. This file composes it with the Mukai vector, so it becomes a function of a numerical class:
N --mukaiVectorHom--> MukaiLattice Λ --extendMap--> ℝ × W × ℝ --expCharge--> ℂ
Every link exists already: mukaiVectorHom is the additive Mukai vector,
extendMap places the integral lattice in the real extension, and expCharge
is Z(β,ω). What the composition buys is that route (A)'s conclusions become
statements about classes rather than about a quadratic space:
numericalCharge_add— the charge is additive in the class, by composition.mukaiForm_neg_of_numericalCharge_eq_zero— the support property in numerical terms: a class killed by the charge has negative Mukai square.numericalCharge_ne_zero_of_nonneg— a class of nonnegative Mukai square is never killed.
What is still not here #
The Mukai vector of an object of Dᵇ(Coh X), and any stability condition.
N is the numerical Grothendieck group and the class map into it is geometry
that lives elsewhere; nothing below constructs a slicing, a heart, or a
Harder–Narasimhan filtration.
The compatibility hf — that the embedding of Λ in its real span carries the
integral form to the real one — is a hypothesis, as it is throughout the lane;
for Λ = NS(X) it says the intersection form is the restriction of its own real
extension.
Z(β,ω) on a numerical class: the charge of the real Mukai vector.
Equations
- D.numericalCharge bR f β ω E = Mukai.expCharge bR β ω (Mukai.extendMap f (D.mukaiVectorHom E))
Instances For
The charge is additive in the class — every link of the composition is.
The charge as a bundled hom, N →+ ℂ.
numericalCharge was proved additive and then left unbundled, which is what kept
the numerical lane from ever meeting the stability-function side: every charge
there is an AddMonoidHom, and an equation is not one. With this the chain from
a numerical class to ℂ is a composition of homs and nothing along it re-proves
additivity.
Equations
- D.numericalChargeHom bR f β ω = AddMonoidHom.mk' (D.numericalCharge bR f β ω) ⋯
Instances For
The charge kills the zero class — free once it is a hom, and absent before.
The real square of a class is half its Mukai square.
The support property, in numerical terms. A class killed by the charge
has negative Mukai square — the statement neg_of_mem_orthogonal becomes once it
is read through the Mukai vector.
A class of nonnegative Mukai square is never killed — there are no walls in the positive cone, said of classes.