Finitely many spherical walls on a Picard-rank-one surface #
Walls/Divisorial/Signature.lean shows that DivisorSpace.HodgeDefinite is the
PeriodDomain.HasSignatureTwo hypothesis, and spends it on Bridgeland's local
finiteness at a point of the period domain. This file instantiates that on the
models of RankOneRealization.lean, so the statement is about a surface rather
than about an abstract quadratic space.
What the statement says #
For a Picard-rank-one surface with ∫H² = h2 > 0, the real Mukai extension is
ℝ ⊕ ℝH ⊕ ℝ and the lattice is the integral Mukai extension
ℤ ⊕ ℤH ⊕ ℤ, which is Mukai.integralExtension of ℤ·H. Then for every
(B, ω) with ω ≠ 0:
only finitely many spherical classes of ℤ ⊕ ℤH ⊕ ℤ
have a wall through the plane of exp(B + iω).
Both hypotheses are discharged. Positivity of ω² is h2 · ω² > 0, and the
signature comes from surfaceHodgeDefinite, which is free on a line. Nothing
is assumed.
Why the rank-one case is the honest first instance #
The Mukai extension of a rank-one divisor space has signature (2, 1), so the
positive planes form a genuine period domain and the finiteness statement is not
vacuous. The two-point blow-up gives signature (2, 3) by the same route, recorded as
BlowUpPlane.hasSignatureTwo; its lattice is not built here, because
Mukai.extendBasis wants an explicit basis of the rank-three divisor space.
Both the pointwise and the region-wise count #
surface_finite_walls_through_expPlane is the count at one plane.
surface_finite_walls_meeting_box is the count over the compact parameter box
|B| ≤ b₀, t₀ ≤ ω ≤ t₁ with t₀ > 0, which is the form a wall-and-chamber
argument consumes. The second needs a uniform coercivity constant, supplied by
PlaneRegion.ofCompactPairs through Divisorial/Region.lean.
What is not proved #
Chambers. Finitely many walls meeting a box does not by itself produce the connected components of its complement, nor constancy of the semistable objects on one.
Nothing here identifies the carrier with K_num(X) for a geometric surface.
The signature of the rank-one Mukai extension #
The real Mukai extension of a Picard-rank-one surface has signature
(2, 1).
This is hasSignatureTwo_of_hodgeDefinite fed with surfaceHodgeDefinite, and
it is what every period-domain theorem has been waiting for.
The degree-2d K3 model, for d > 0.
The lattice #
The ℝ-basis of the rank-one divisor line.
Instances For
The induced basis of the real Mukai extension ℝ ⊕ ℝH ⊕ ℝ.
Equations
Instances For
The ℤ-span of that basis is the integral Mukai extension ℤ ⊕ ℤH ⊕ ℤ.
This is what makes the finiteness statement below one about integral classes.
Local finiteness of spherical walls #
Only finitely many spherical classes of the integral Mukai lattice have a
wall through the plane of exp(B + iω), on a Picard-rank-one surface with
∫H² > 0.
Both hypotheses of the generic theorem are discharged here: ω² = h2 · ω² > 0
because ω ≠ 0, and the signature by surfaceHasSignatureTwo.
The same, on the degree-2d K3 model.
The K3 statement with the lattice named as the integral Mukai extension
ℤ ⊕ ℤH ⊕ ℤ rather than as a span of basis vectors.
Region-wise finiteness over a compact parameter box #
The compact family of parameters |B| ≤ b₀, t₀ ≤ ω ≤ t₁. Any compact set
on which ω stays away from zero would do; a box is the readable choice.
Equations
Instances For
Only finitely many spherical classes of the integral Mukai lattice have a
wall meeting the parameter box, on a Picard-rank-one surface with ∫H² > 0.
This is the region-wise statement, the one a wall-and-chamber argument consumes.
Both hypotheses of the generic theorem are discharged: the box is compact, and
ω² = h2 · ω² > 0 because ω ≥ t₀ > 0.
The region-wise count on the degree-2d K3 model, with the lattice named
as the integral Mukai extension ℤ ⊕ ℤH ⊕ ℤ.
Nothing is assumed beyond d > 0 and t₀ > 0.
The chamber of the box, cut out by finitely many walls #
The bounded region of the parameter box, in the (β, ω) chart. This is the
first witness for Spherical.BoundedRegion on a surface.
Equations
Instances For
Finitely many spherical classes of the lattice have a wall meeting the
box, in the (β, ω) chart of a Picard-rank-one surface.
On the box, the chamber of the whole lattice is the chamber of those finitely many classes.
This is the chamber decomposition, on a surface, with every hypothesis
discharged. It says nothing about semistable objects: chamber is a subset of
the parameter chart.
The same on the degree-2d K3 model, assuming only d > 0 and t₀ > 0.