Walls and chambers on the two-point blow-up #
BlowUpPlane.lean proves the hard part for this model and gets none of the
consequences. It has hodgeDefinite — the reverse Cauchy--Schwarz inequality
for diag(1, -1, -1), so the intersection form is negative definite on the
plane ω^⊥ — and hasSignatureTwo follows. But it has no basis of the
rank-three divisor space, so nothing downstream reaches it:
Mukai.extendBasis wants one, and without a lattice there is no wall count, no
region, and no chamber.
RankOneWalls.lean has all of that on the line. But in Picard rank one the
Hodge input is vacuous: the orthogonal complement of a nonzero vector on a
line is zero, so the definiteness clause says nothing. This model is the one
where it says something, which makes it the model where the wall statements
have content.
This file supplies the basis and instantiates the chain.
What lands #
divisorBasis— the missing ingredient,H, E₁, E₂as anℝ-basis.span_mukaiBasis— its extension spans the integral Mukai extensionℤ ⊕ (ℤH ⊕ ℤE₁ ⊕ ℤE₂) ⊕ ℤ, which is the lattice the counts are stated against.finite_walls_through_expPlane— the pointwise count.finite_walls_meeting_ampleBox— the region-wise count over a compact family.boxRegion,signedRayRegularLocus_inter_ampleBox— the chamber, cut out by finitely many walls on the family.
Every hypothesis is discharged. Because hodgeDefinite needs only ω² > 0 on
this surface, so does everything below: no separate Hodge certificate is carried.
The compact family #
ampleBox ω₀ b₀ t₀ t₁ is ‖B‖ ≤ b₀ together with ω on the segment
[t₀, t₁]·ω₀ of the ray through a fixed class of positive square. Scaling a
fixed ω₀ keeps ω² = t²·ω₀² > 0 for t ≥ t₀ > 0, which is the only thing the
region needs. RankOneWalls.parameterBox is the same shape specialised to the
line; each example states its own, as examples do.
What is not claimed #
Nothing about semistable objects. chamber is a subset of the parameter chart,
and no constancy on it is asserted. The carrier is not identified with
K_num(X) for a geometric blow-up, and no Hodge index theorem is proved for
one — hodgeDefinite is proved for this lattice, which is the whole point.
The basis of the rank-three divisor space #
The missing ingredient: H, E₁, E₂ as an ℝ-basis of the divisor
space.
Equations
Instances For
The induced basis of the real Mukai extension ℝ ⊕ N¹_ℝ ⊕ ℝ.
Equations
Instances For
The ℤ-span of that basis is the integral Mukai extension of the
Néron--Severi lattice ℤH ⊕ ℤE₁ ⊕ ℤE₂. This is what makes the counts below
statements about integral classes.
The pointwise count #
Only finitely many spherical classes of the lattice have a wall through
the plane of exp(B + iω), on the two-point blow-up.
The only hypothesis is ω² > 0. On this surface hodgeDefinite needs nothing
more, so neither does the finiteness.
A compact family along an ample ray #
The compact family ‖B‖ ≤ b₀, ω ∈ [t₀, t₁]·ω₀.
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.ampleBox omega₀ b₀ t₀ t₁ = Metric.closedBall 0 b₀ ×ˢ ((fun (t : ℝ) => t • omega₀) '' Set.Icc t₀ t₁)
Instances For
On the family ω² stays positive, because scaling a class of positive
square by t ≥ t₀ > 0 scales the square by t².
The region-wise count, and the chamber #
The region-wise count. Only finitely many spherical classes of the lattice have a wall meeting the family.
The bounded region of the family, in the (β, ω) chart.
Equations
Instances For
Finitely many spherical classes have a wall meeting the family, in the
(β, ω) chart.
On the family, the chamber of the whole lattice is the chamber of those finitely many classes.
This is the chamber decomposition on the model where the Hodge input is not vacuous. It says nothing about semistable objects.
The integral Néron--Severi lattice, and the spherical comparison #
The integral Néron--Severi lattice of the two-point blow-up:
ℤH ⊕ ℤE₁ ⊕ ℤE₂ in coordinates.
Equations
Instances For
The integral intersection form diag(1, -1, -1). This is the rational form
of BlowUpPlane.lean read over ℤ, and the blow-up had no integral lattice
before.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion of the integral lattice into the real divisor space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second witness for Spherical.IntegralComparison, and the one where
the form is not definite.
The obligation that structure records — "exhibiting NS(X) with its
intersection form" — is discharged here by ℤH ⊕ ℤE₁ ⊕ ℤE₂ with
diag(1, -1, -1). Unlike the rank-one case, the lattice has isotropic vectors
and the comparison is not a scaling of ℤ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Integral and real sphericality agree in the (β, ω) chart, on the
two-point blow-up.
The realized anticanonical class is the image of the integral class
3H - E₁ - E₂, so the ray the chamber statements use is an integral one.
The anticanonical ray #
The realized anticanonical class -K = 3H - E₁ - E₂ has square 7, so it
is an admissible ω₀.
The chamber decomposition along the anticanonical ray, with every hypothesis discharged and nothing supplied.