The correction slot at √td: the transport there is the Mukai charge #
PolarisedWallTransport.lean carries a correction class κ as a parameter and
says of it that κ = 1 gives the plain Chern character and κ = √td gives the
Mukai vector. Only the first of those had an inhabitant. corrComp_sqrtToddComp
proved the class map at √td is mukaiComp by rfl, but nothing tied the
resulting charge to the Mukai charge the repository already had, so the
claim that κ = √td produces the K3 Mukai charge rested on a docstring.
This file proves it, for an arbitrary surface realization and with no K3 hypothesis. The K3 statement is a corollary.
Why the comparison is pointwise, and why that is not a weakness #
No equality of ChargeFamilys is statable here, and the reason is structural
rather than a shortfall of the proof. Polarised.wallChargeFamily is indexed
by ℂ; mukaiCharge is indexed by StabilityParameters D, a pair of
independent divisor classes. The two carriers sit over different data bundles,
and the map between the parameter spaces exists only on the rank-one slice
B = sH, ω = tH, where Surface.NumericalRealization.rankOneParameters
already provides it. So the comparison is stated pointwise on that slice,
exactly as wallChargeFamily_charge_eq_centralCharge states the κ = 1 case.
κ = 1 and κ = √td are two pullbacks, not one family #
They are genuinely different walls and must not be fused. The difference is
mukaiCharge_eq_centralCharge_add (Walls/Divisorial/Mukai.lean), which is
linear in the class and nonzero whenever √td is: on a K3 it shifts the third
Mukai coordinate by the rank, which is what turns (r, c₁, ch₂) into
Bridgeland's (r, c₁, ch₂ + r).
SqrtTodd is an image, not a truncation #
Wall.Divisorial.SqrtTodd keeps a codimension-one class and one real number.
It is what a realization of κ can see, not a truncation of κ itself: the
map forgetting slots 0 and above 2 is lossy, and √td₀ = 1 is dropped by
it rather than preserved. NumericalRealization.sqrtTodd (DivisorialMukai.lean)
is that image, and the three slot lemmas below are where the loss is accounted
for — slot 0 reappears as the ∫H² weight and nowhere else.
Main results #
hDegrees_sqrtToddComp_eq_mukaiVector— the transported degrees atκ = √tdare the compressed Mukai vector. This is the whole content; the charges then agree because they are the same polynomial.wallChargeFamily_sqrtToddComp_eq_mukaiCharge— the comparison, for any surface realization.wallChargeFamily_sqrtToddComp_eq_mukaiCharge_k3— the K3 corollary, throughmukaiCharge_of_isK3.
The realized polarisation pairs with any realized codimension-one class to
that class's rational H-degree. pair_realizePolarization_chOne
(DivisorialWallTransport.lean) is the ch₁ case of this; √td₁ needs the
same fact and is not a Chern component.
Pairing the realized polarisation against a realized class plus a real
multiple of another. This is the exact shape slot 1 of the Mukai vector takes:
c₁ + r·√td₁, with the scalar a real rank rather than a rational one.
The transported degrees at κ = √td are the compressed Mukai vector.
Slot by slot: ∫H²·r, ∫H·(c₁ + r√td₁), and ∫(ch₂ + ch₁√td₁ + r√td₂). The
middle and last are the two places √td enters, and the first is where the
polarisation weight lives — √td₀ = 1 contributes there and is invisible in
SqrtTodd, which is the loss the module docstring names.
The correction slot has a real inhabitant.
The polarised transport at κ = √td, on the rank-one slice B = sH, ω = tH,
is the repository's Mukai charge. No K3 hypothesis: this holds for every
surface realization, and the K3 case is the corollary below.
Both sides are the same exponential polynomial — the left through
Exp.charge on compressed degrees, the right through Mukai.expCharge on the
intersection form — so once the degrees are known to be the Mukai vector
(hDegrees_sqrtToddComp_eq_mukaiVector) the charges agree by the rank-one
collapse of the keystone.
The K3 corollary. On a K3 the transport at κ = √td is the ordinary
divisorial charge minus the rank.
It is a corollary and not the statement: mukaiCharge_of_isK3 is what supplies
√td = 1 + [pt], and the comparison above holds without it.
The two correction values are not one family #
The block above needs a realization, because mukaiCharge lives on a real
divisor space. The statement below needs none: it compares the two values of
κ against each other, and both sides are built from V and P alone.
On a K3 the √td-corrected degrees are the plain ones with the rank added
to the last slot, and nothing else moved.
√td₁ = 0 is what leaves slots 0 and 1 alone, and ∫√td₂ = 1 is what puts
exactly the rank into slot 2. Those are K3.sqrtToddComp_one and
K3.degree_sqrtToddComp_two; no other K3 input is used.
The two correction values give different charges, and the difference is the rank.
On a K3 the κ = √td transport is the κ = 1 transport of
WallTransport.lean minus the rank — an additive term linear in the class, so
the two are not a reparameterisation of each other and their walls genuinely
differ. This is what makes "do not fuse the two pullbacks" a theorem rather
than a warning in a docstring.
No realization appears: both sides are built from V and P.