The Mukai exponential charge on an HN-tilted heart #
Mukai.Slope reads the sign of Im Z(β,ω) against the cutoff classes of the
untilted heart. WeakHnTilt.lean builds the tilt. This file joins them: every object of
the tilted heart has 0 ≤ Im Z(β,ω).
The obstruction this removes #
MukaiChargeData carries mukai : K₀Ab A →+ Mukai.RealExtension V — a charge on an abelian
category. The tilted heart's objects are ambient: hnTilt_heart_iff presents X : C inside a
triangle F₀⟦1⟧ → X → T₀, and only F₀ and T₀ lie in t.heart. So nothing could be said
about Z(X) at all: the additivity was available, the charge was not.
The fix is a restriction, not a hypothesis. Take the charge on K₀ C as the primitive and
define the heart datum by composing with K₀Ab.toAmbient (GrothendieckGroup/HeartComparison.lean).
Compatibility is then rfl rather than a field, so there is no new structure to inhabit and no
new assumption to discharge — which is the failure mode Mukai.Charge warns about and that the
single-instantiation gate now catches.
Note this uses only the map K₀Ab 𝒜 →+ K₀ C. The isomorphism K(𝒜) ≅ K(D) is
unavailable at this pin and is not assumed; HeartComparison.lean says so, and nothing here needs
it.
The argument #
K₀.of_triangle and K₀.of_shift_one give Z(X) = -Z(F₀) + Z(T₀). #808 bounds the two ends —
Im Z(T₀) ≥ 0 because T₀ is torsion, Im Z(F₀) ≤ 0 because F₀ is torsion-free — and the
signs combine. The zero object is handled separately at each end, where the charge vanishes.
What this is still not #
It is not Bridgeland's Lemma 6.2. Lemma 6.2 needs the charge in
semiClosedUpperHalfPlane — Im > 0, or Im = 0 and Re < 0. This supplies only the
imaginary half for arbitrary tilted-heart objects. The adapters below close the
strict-below, positive-rank torsion, dimension-zero, and boundary-generator cases
when their numerical hypotheses are supplied explicitly.
The remaining geometric and torsion work is outside this lane:
- the exact-margin and uniform-lower-bound boundary theorems both take their
numerical inequality as a hypothesis. The assembly-safe adapter takes it
factorwise; for K3 surfaces, supplying
realForm ≥ -1for eachμ-stable factor is the paper's Lemma 5.1 — Serre duality, Riemann--Roch, finite-dimensionalHom— which is not in this repository (#332); - the torsion cases split by dimension of support and use ampleness, and
WeakSlopeDatacarries a rank and a degree and nothing else.
Neither is a case analysis, and nothing here pretends otherwise.
The zero-dimensional torsion numerical shadow.
If a heart object has Mukai class (0, 0, s) with 0 < s, its ambient
charge lies on the negative real ray. The class equation is an explicit
support-dimension input; this theorem does not assert that an arbitrary
rank-zero object has that class.
Every object of the tilted heart has 0 ≤ Im Z(β,ω).
The imaginary half of Bridgeland's Lemma 6.2, on the tilted heart. The triangle
F₀⟦1⟧ → X → T₀ of hnTilt_heart_iff splits the charge; #808 signs the two ends; the shift
flips the torsion-free one so both contributions are nonnegative.
This is not Lemma 6.2: that needs Re < 0 on the Im = 0 boundary, which is blocked on
Lemma 5.1 and on dimension-of-support data. See the module docstring.
The strict-below free-generator case of the upper-half-plane argument.
If F₀ is a nonzero object of the weak HN torsion-free class at the cutoff and its
slope is strictly below b β ω, then the shifted object F₀⟦1⟧ has ambient charge in
semiClosedUpperHalfPlane. The proof exposes the paper's sign convention: the
charge of F₀ has negative imaginary part, and the shift negates it.
This closes only the strict-below generator case (case 3), not the full Lemma 6.2
theorem. The boundary equality case and the rank-zero torsion/point cases still
need the geometric Mukai-square and support-dimension inputs described in the module
docstring. MukaiWeakSlopeCompat contributes only the rank/degree compatibility;
no K3 or Bogomolov--Gieseker statement is assumed here.
The positive-rank HN-torsion generator case.
An object of the weak HN torsion class with positive rank has strictly positive
imaginary charge by MukaiWeakSlopeCompat. This is the open-upper-half-plane
part of the untilted torsion generator; rank-zero torsion is intentionally left
for a separate support-dimension input.
The boundary free-generator case from factorwise real positivity.
This is the parent of every boundary theorem below, and it contains no Hodge
theory. Given a nonempty family G of positive-rank factors at the cutoff whose
Mukai classes sum to the class of F₀, each factor has Im Z = 0 by slope
arithmetic, and the supplied 0 < Re Z per factor is all the additive step
needs. How that positivity is obtained — the exact Hodge margin, a uniform
quadratic lower bound, or any other route — is the consumers' business.
Real positivity from the exact Hodge margin. A positive-rank object at
the cutoff whose class makes 2 * realForm b v + rank(v)² * ω² positive has
Re Z > 0: this is Mukai.re_expCharge_pos_of_boundary_margin read through
the rank and slope identifications.
Real positivity from a uniform quadratic lower bound. Integrality of the
rank turns 0 < rank into 1 ≤ rank, so the single polarisation inequality
2δ < ω² suffices for every factor with realForm ≥ -δ.
The boundary free-generator case under the exact factorwise Hodge
margin. Each factor's margin gives its real positivity by
re_charge_pos_of_margin; the parent
mem_semiClosedUpperHalfPlane_of_shift_of_boundary_factors_of_re_pos adds.
The boundary free-generator case for an arbitrary factorwise lower bound.
G is the nonempty family of boundary factors whose Mukai classes sum to the
class of F₀. Positive rank and equality with the cutoff force every factor's
imaginary charge to vanish; the Mukai-square hypothesis is imposed separately
on every factor, and re_charge_pos_of_lower_bound turns it into real
positivity before the parent theorem adds.
A geometric consumer instantiates G with stable factors, supplies a uniform
lower bound realForm ≥ -δ, and proves the corresponding polarization
threshold 2δ < ω². Bridgeland's K3 argument is the specialization δ = 1;
the factorization itself does not own that constant.
The K3-normalized boundary-factor theorem, recovered at δ = 1.
The assumption ω² > 2 supplies both positivity of the polarization and the
uniform threshold 2δ < ω². New geometric children should use
mem_semiClosedUpperHalfPlane_of_shift_of_boundary_factors_of_lower_bound
and state their own lower bound.
Low-level one-class boundary adapter with an arbitrary explicit lower bound.
If the weak HN torsion-free generator lies exactly on the cutoff, the imaginary
part vanishes. The supplied bound -δ ≤ Mukai.realForm, together with
2δ < ω², puts the shifted charge on the allowed negative real ray.
The Mukai-square bound is intentionally a theorem input rather than a field of
MukaiChargeData. This theorem is useful when a bound on the whole class is
already available, but it is not the final assembly seam: a quadratic
lower bound on v² is not preserved by extensions. Use
mem_semiClosedUpperHalfPlane_of_shift_of_boundary_factors_of_lower_bound when
the bound is known only for stable factors.
The historical one-class K3 boundary adapter, obtained from the arbitrary
lower-bound theorem with δ = 1.