Numerical intersection data for the blow-up of P² at two points #
The first model in this repository of Picard rank greater than two. For
X = Bl_{p,q} P² the numerical divisor lattice is
N¹(X) = ℤH ⊕ ℤE₁ ⊕ ℤE₂, H² = 1, E₁² = E₂² = -1,
with all other products zero, so the intersection form is diag(1, -1, -1):
signature (1, 2). This is the smallest example in the Mizuno--Yoshida family
in which ω^⊥ is a genuine negative definite plane rather than a point,
which is what makes it worth building.
Why rank three and not rank two #
SmoothQuadric.lean already has Picard rank two, but its form is hyperbolic
and its ω^⊥ is a line. RankOneRealization.lean has ω^⊥ = 0, so
DivisorSpace.HodgeDefinite there is vacuous in its definiteness clause. Here
the clause has content: blowUpHodgeDefinite is the reverse Cauchy--Schwarz
inequality for diag(1,-1,-1), and it is proved, not supplied. That is the
first time in this library that the Hodge input to the support property of
Stability/DivisorialSupport.lean is discharged by a real argument.
The ring #
The rational intersection ring is ℚ ⊕ N¹_ℚ ⊕ ℚ with
(a, v, s)(a', v', s') = (aa', av' + a'v, as' + a's + v·v').
It is built here as a bespoke five-field carrier rather than as a quotient of a
polynomial ring, because the graded basis 1, H, E₁, E₂, pt then holds by
decide on each pair instead of needing a normal form for an ideal. The
nested-dual-number trick of SmoothQuadric.lean does not extend: it produces a
hyperbolic form, and diag(1,-1,-1) is not hyperbolic.
The lattice, and why ch₂ is reparametrized #
ch₂ is a half-integer here, exactly as on P². For D = aH + bE₁ + cE₂ the
line bundle O(D) has ch₂ = (a² - b² - c²)/2. Coordinates (r, a, b, c, v)
therefore record
ch₂ = (a + b + c)/2 + v,
which is the shift that makes χ = r + 2a + b + c + v integral, the same device
ProjectivePlane.lean uses with ch₂ = c/2 + v.
What is not claimed #
The carrier is not identified with K_num(X) for a geometric blow-up, and no
Chern-character map from coherent sheaves is constructed. Ampleness enters only
as the numerical condition ∫(ω²) > 0; the actual ample cone
a > b + c, b > 0, c > 0 is recorded but not required by any theorem below.
The rational intersection ring #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The intersection product: diag(1, -1, -1) on the divisor coordinates,
landing in the point class.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The rational scalars, as a ring map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The named classes #
The hyperplane class pulled back from P².
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.hQ = { const := 0, hCoeff := 1, e₁Coeff := 0, e₂Coeff := 0, ptCoeff := 0 }
Instances For
The first exceptional class.
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.e₁Q = { const := 0, hCoeff := 0, e₁Coeff := 1, e₂Coeff := 0, ptCoeff := 0 }
Instances For
The second exceptional class.
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.e₂Q = { const := 0, hCoeff := 0, e₁Coeff := 0, e₂Coeff := 1, ptCoeff := 0 }
Instances For
The point class.
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.pointQ = { const := 0, hCoeff := 0, e₁Coeff := 0, e₂Coeff := 0, ptCoeff := 1 }
Instances For
The graded basis #
The product basis 1, H, E₁, E₂, pt.
Equations
Instances For
Membership of the named classes #
The rational numerical intersection ring of the two-point blow-up.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The numerical lattice #
Numerical classes in the coordinates (r, a, b, c, v), with
ch₁ = aH + bE₁ + cE₂ and ch₂ = (a + b + c)/2 + v.
Equations
Instances For
The Chern-character components in the blow-up intersection ring.
Equations
- One or more equations did not get rendered due to their size.
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.chComp E 0 = (algebraMap ℚ AlgebraicGeometry.Numerical.Examples.BlowUpPlane.Ring) ↑(E 0)
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.chComp E 2 = ((↑(E 1) + ↑(E 2) + ↑(E 3)) / 2 + ↑(E 4)) • AlgebraicGeometry.Numerical.Examples.BlowUpPlane.pointQ
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.chComp E n.succ.succ.succ = 0
Instances For
Todd class, Euler characteristic, and the variety #
The Todd class of the two-point blow-up: td₁ = -K/2 = (3H - E₁ - E₂)/2 and
td₂ = pt, so ∫td₂ = χ(O_X) = 1.
Equations
- One or more equations did not get rendered due to their size.
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.toddComp 0 = 1
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.toddComp 2 = AlgebraicGeometry.Numerical.Examples.BlowUpPlane.pointQ
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.toddComp n.succ.succ.succ = 0
Instances For
The total Chern character in the five explicit coordinates.
The total Todd class in the five explicit coordinates.
The Euler characteristic in the chosen integral coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The model. The blow-up of P² at two points, of Picard rank three.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presentation satisfies Hirzebruch--Riemann--Roch:
χ = r + 2a + b + c + v.
Polarizations #
A rational divisor class aH + bE₁ + cE₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Not a simp lemma: degree_apply is already simp and rewrites the
left-hand side to a ptCoeff projection first, so the normal-form linter
rejects the attribute.
The ample cone of the two-point blow-up, recorded for the reader:
aH - bE₁ - cE₂ is ample exactly when b > 0, c > 0 and a > b + c. No
theorem below needs it; the numerical condition that matters is ∫(ω²) > 0.
Equations
Instances For
A polarization from coefficients of positive square.
Equations
- AlgebraicGeometry.Numerical.Examples.BlowUpPlane.polarization a b c h = { cls := AlgebraicGeometry.Numerical.Examples.BlowUpPlane.polarizationClass a b c, cls_mem := ⋯, degree_pow_pos := ⋯ }
Instances For
The anticanonical polarization -K = 3H - E₁ - E₂, of square 7.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real divisor space #
Real numerical divisor classes, in the basis H, E₁, E₂.
Instances For
The intersection form diag(1, -1, -1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The rank-three real divisor space of the two-point blow-up.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The realization #
The codimension-one piece is the rational span of H, E₁, E₂.
Every class of codimension one has vanishing constant term. This is the only fact about the piece the realization needs.
The realization of a rational divisor class in the basis H, E₁, E₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The real divisor realization of the two-point blow-up.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Hodge index theorem in signature (1, 2) #
Hodge definiteness on the two-point blow-up is exactly positivity of
ω².
This is the reverse Cauchy--Schwarz inequality for diag(1, -1, -1): if
ω² > 0 and x ⊥ ω with x ≠ 0, then x² < 0. Unlike the rank-one models,
the definiteness clause here has content, because ω^⊥ is a plane.
It is proved, not supplied. That is what makes the support property of
Stability/DivisorialSupport.lean depend on Bogomolov--Gieseker alone on this
surface.
The realized anticanonical polarization has square 7, so it is a Hodge
class in the sense above.
The real Mukai extension of the two-point blow-up has signature
(2, 3).
hodgeDefinite is exactly the input hasSignatureTwo_of_hodgeDefinite wants,
so every period-domain theorem — the negative definiteness on the orthogonal
complement of a positive plane, the wall-finiteness statements, the orientation
cocycle — is available here from ω² > 0 alone.
The support property, needing Bogomolov--Gieseker alone #
On the two-point blow-up the support property reduces to Bogomolov--Gieseker.
hasQuadraticSupportProperty_semistable takes two supplied inputs. Here the
Hodge input is discharged by hodgeDefinite, so the only hypothesis left is a
BogomolovGiesekerData and positivity of ω². That is the payoff of building
a model whose intersection form has signature (1, 2).
The same conclusion in the norm-bound formulation.