Transporting a polarised surface class to the (s, t) plane #
Walls/Numerical/Basic.lean does all its wall geometry on NumClass, a triple
of reals, and says of it: "It is not ch(E) for a sheaf E." This file
supplies the map that makes it one, on the AlgebraicGeometry side where both
halves are visible, and spends Bogomolov–Gieseker to discharge the two
hypotheses that file declines to assume.
The normalisation, derived rather than guessed #
Basic.lean's charge is
reZ s t v = -v.ch2 + s·v.deg - (s²/2)·v.rk + (t²/2)·v.rk, imZ s t v = t·(v.deg - s·v.rk)
Matching term by term against the surface tilt charge
Z_{β,α}(E) = -∫ch₂^β + (α²/2)·∫H²·ch₀ + i·∫H·ch₁^β, s = β, t = α
forces
rk ↔ ∫H² · rank(E) deg ↔ ∫c₁(E)·H ch2 ↔ ∫ch₂(E)
The rank slot is weighted by ∫H². That is the content of this file and
the thing to get right.
Why the naive reading is wrong #
Taking (rank E, ∫c₁·H, ∫ch₂) does not satisfy the charge formula, and its
NumClass.discr is (∫c₁·H)² − 2·rank·∫ch₂, which is neither ∫Δ(E) nor
anything Bogomolov–Gieseker bounds. Turning it into ∫Δ(E) would need
(∫c₁·H)² = ∫c₁², which is equality in Hodge index together with ∫H² = 1.
So discr_toNumClass is stated against Surface.discrH, not against
∫Δ(E). An earlier draft of this lane claimed the latter; it is false, and it
fails on this lane's own K3 witness — 4d²c² against 2dc². Recorded here so
the mistake is not made a third time.
With the weighted reading the identity is exact: discr of the transported
class is Surface.discrH, and Surface.discrH_nonneg supplies its
nonnegativity for a semistable class.
The bridge is one-way #
This is the first module to import the Walls lane from AlgebraicGeometry,
and the direction is the permitted one. Nothing under CategoryTheory/** is
edited or added to; if a lemma were needed there it belongs in the wall lane,
not here, and scripts/check_layering.py holds the boundary.
Every declaration quantifies over N. Nothing here says a wall is a wall for
an object, that an object changes semistability across one, or anything about
mass or Hom.
This is the H-slice, not the full wall family #
toNumClass keeps only ∫c₁·H, so on a surface of Picard rank greater than
one it discards the components of c₁ orthogonal to H. The resulting
wallChargeFamily is the (s,t)-plane B = sH, ω = tH of the divisorial
family, and nothing more; two classes with different c₁ but the same
H-degree are indistinguishable here (Altavilla, arXiv:1905.10636, §2.2).
The arbitrary-(B,ω) family lives in DivisorialWallSlice.lean, and
DivisorialWallTransport.lean proves that this file's family is its rank-one
reindexing.
Main results #
Surface.toNumClassand its three component lemmas, plustoNumClass_add.Surface.toNumClassHomandSurface.wallChargeFamily— the additive pullback that places every polarised surface below the generic wall root.Surface.discr_toNumClass— the identity the bridge turns on.Surface.toNumClass_ne_zero_of_rank_ne_zero— nonzero rank suffices.Surface.charge_ne_zero_of_semistable— the charge hypothesis, discharged.Surface.wall_eq_of_meet_of_semistable— walls disjoint, with no excluded point.Surface.walls_nested_of_semistable— walls nested, within a family.Examples.toNumClass_k3andExamples.discr_toNumClass_k3— the worked instance, with the∫H² = 2dfactor visible on both sides.
A polarised surface class as a point of the (s, t) wall plane.
The rank slot carries ∫H²; see the module docstring for the term-by-term
derivation, and for why the unweighted reading does not satisfy the charge
formula.
Equations
Instances For
The transport is additive, because rank, degH and ch₂ all are.
The numerical-class transport bundled as an additive map.
Bundling is what lets the surface model inherit generic wall constructions by
ChargeFamily.pullback, rather than rebuilding wall equations for each
surface presentation.
Equations
Instances For
The (s,t) numerical wall family pulled back to any polarised surface
presentation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Surface walls are inherited pullbacks of the generic determinant, whose
specialized value is the established (s,t) polynomial.
The identity the bridge turns on. The wall-plane discriminant of a
transported class is exactly the tilt discriminant Surface.discrH.
Both sides are deg² − 2·rk·ch₂ once the transport is unfolded, so this is a
match of conventions rather than a computation — but it is a match that only
holds with the ∫H² weight in the rank slot.
Not ∫Δ(E): see the module docstring.
A class of nonzero rank transports to a nonzero triple: the rank slot is
∫H² · rank E, and ∫H² > 0 is the Polarization's own field.
Spending Bogomolov–Gieseker on the wall structure #
The transported discriminant of a semistable class is nonnegative — the
composite of discr_toNumClass with Surface.discrH_nonneg.
The charge hypothesis of wall_eq_of_meet, discharged.
Basic.lean states it as a hypothesis because, in its words, "Δ ≥ 0 is a
theorem about sheaves and NumClass is a triple". Here the class comes from a
sheaf-level datum, so the theorem is available and the hypothesis is not needed.
The only t-dependence left is t ≠ 0, which is the half-plane condition.
Distinct numerical walls of a semistable class of nonzero rank are disjoint, with no excluded point.
This is wall_eq_of_meet with its charge hypothesis supplied rather than
assumed. Nonzero rank is what makes the class a nonzero triple.
Bertram nesting for a semistable geometric class.
walls_nested_of_discr_nonneg with 0 ≤ discr supplied by Bogomolov–Gieseker
instead of hypothesised. The same-family hypothesis is kept: it is load-bearing,
and the wall lane carries the counterexample that shows so. The minA ≠ 0 and
0 ≤ wallRadiusSq hypotheses are kept too — nothing here discharges them.
The worked instance #
The transport on the rank-one K3 model, evaluated. Every slot carries the
polarisation degree ∫H² = 2d: the rank slot by the weighting, the degree slot
through degH, and ch₂ through ∫H² in surfaceDegree.
The rank-one K3 model as a concrete child of the generic wall-family hierarchy, through the polarised-surface transport.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The K3 child evaluates through the degree-weighted numerical triple.
Both sides of discr_toNumClass on the K3 model, as one explicit rational:
Δ = 4d²·(E 1)² − 8d²·(E 0)·(E 2).
The ∫H² = 2d factor is present twice on the rank–ch₂ term and squared on the
degree term, which is exactly the weighting the naive transport would lose.