The real divisor realization of a Picard-rank-one surface, and the K3 model #
Models/Surface/RankOne.lean builds the rational intersection ring
ℚ[H]/(H³) with ∫_X H² = h2, and K3.lean, ProjectivePlane.lean and
Abelian.lean are three variety presentations over it. What none of them had
was a Surface.NumericalRealization: a map of the rational codimension-one
piece into a real divisor space carrying the intersection form. Without one,
every divisorial statement — the charge, the discriminants, the walls, the
support property — was conditional on a realization existing at all.
This file supplies it once, for every h2, and then instantiates the K3 case.
The realization #
The rational piece N¹ is the line ℚ·H, so the real divisor space is ℝ
with H as the unit vector and the intersection form
(x, y) ↦ h2 · x · y.
surfaceRealization packages that, and surfaceChernCharacter_* reads off the
induced real Chern character in the coordinates (r, c, s) of SurfaceNum:
rank r, first Chern class c, and ∫ch₂ = h2 · s. The last one is worth
stating explicitly, because SurfaceNum records the coefficient of H² and
the divisorial layer wants its integral.
Hodge definiteness is free in Picard rank one #
DivisorSpace.HodgeDefinite asks for ω² > 0 together with negative
definiteness on ω^⊥. On a line with a nondegenerate form the orthogonal
complement of a nonzero vector is zero, so the second condition holds with no
content and the first is h2 · t² > 0. surfaceHodgeDefinite is therefore a
theorem, not a supplied certificate, and it is what makes the support property
of Stability/DivisorialSupport.lean fire on a model rather than on a
hypothesis.
That is the whole point of doing rank one first: it separates "the support
property argument is correct" from "the Hodge input is available", and only the
second is hard. A Picard rank three example, where ω^⊥ is a genuine negative
definite plane, is the next step and lives in BlowUpPlane.lean.
What is not claimed #
The carrier is not identified with K_num(X) for a geometric K3, and no
Chern-character map from coherent sheaves is constructed. The
Bogomolov--Gieseker input is k3BogomolovSanity, whose Semistable predicate
is defined to be the conclusion; the support property below is therefore a
statement about the locus of classes of nonnegative discriminant, which is
exactly what it says, and it is not a theorem about semistable sheaves.
The real divisor line #
The real numerical divisor space of a Picard-rank-one surface: the line
spanned by H.
Instances For
The intersection form (x, y) ↦ h2 · x · y in the basis H.
Equations
- AlgebraicGeometry.Numerical.Examples.surfaceIntersectionForm h2 = LinearMap.mk₂ ℝ (fun (x y : AlgebraicGeometry.Numerical.Examples.SurfaceDivisor) => h2 * x * y) ⋯ ⋯ ⋯ ⋯
Instances For
The real divisor space of a Picard-rank-one surface with ∫_X H² = h2.
Equations
- AlgebraicGeometry.Numerical.Examples.surfaceDivisorSpace h2 = { intersection := AlgebraicGeometry.Numerical.Examples.surfaceIntersectionForm h2, intersection_symm := ⋯ }
Instances For
The rational divisor piece is the line ℚ·H #
The index of H in the power basis.
Equations
Instances For
The codimension-one piece is the rational line spanned by H.
The realization #
The H-coordinate of a rational divisor class, as a real number.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Multiplication in the rational ring realizes to the intersection form
h2 · x · y.
The real divisor realization of a Picard-rank-one surface.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The realization sends H to the unit vector.
Hodge definiteness in Picard rank one #
Negative definiteness on ω^⊥ is free on a line.
The orthogonal complement of a nonzero vector for a nondegenerate form on ℝ
is 0, so the definiteness clause is vacuous and only positivity of ω²
carries content.
The K3 model #
The realization of the degree-2d K3 model.
Equations
Instances For
The realized polarization of the K3 model is the unit vector H.
The real Chern character of the K3 model: rank E 0, first Chern class
E 1, and ∫ch₂ = 2d · E 2.
Not a simp lemma: the generic NumericalRealization.chernCharacter_*
lemmas are already simp and rewrite the left-hand side first, so the
normal-form linter rejects the attribute.
Not a simp lemma: the generic NumericalRealization.chernCharacter_*
lemmas are already simp and rewrite the left-hand side first, so the
normal-form linter rejects the attribute.
Hodge definiteness holds on the K3 model at every nonzero real multiple
of H, with d > 0.
The support property, on a model rather than on hypotheses #
The divisorial charge of the degree-2d K3 model has the quadratic
support property on the locus of classes of nonnegative discriminant, at every
(B, ω) with ω a nonzero real multiple of H.
Both inputs of hasQuadraticSupportProperty_semistable are discharged here.
The Hodge input is k3HodgeDefinite, which is proved. The Bogomolov input is
k3BogomolovSanity, whose Semistable predicate is defined to be
0 ≤ discDegH, so the locus below is exactly the nonnegative-discriminant
locus and no claim is made about semistable sheaves.
What is not tautologous is the conclusion: negative definiteness of the
C-discriminant on the kernel of the charge is genuine content, and it is what
the support property needs.
The same conclusion in the norm-bound formulation.
The Mukai vector of the model #
The realized square root of the Todd class of the model is 1 + [pt].
This is sqrtTodd_eq_k3 fired on a presentation that exists.
Bridgeland's K3 charge on the model is the divisorial charge minus the rank.