The Mukai data of the rank-one K3 model #

GrothendieckGroup/MukaiVector.lean says in its own "What this file does not assert" section that nothing constructs an IntegralMukaiData and nothing constructs an AdditiveMukaiData. This file meets that hypothesis, on the degree-2d rank-one model k3NumericalVariety d, with

Λ = ℤ        c₁(E) = E 1        b x y = 2d·x·y

What an inhabitant buys, without a line changing anywhere else #

Every consumer of IntegralMukaiData on main takes one as a hypothesis, so each is a statement about a structure nothing was known to satisfy. Supplying one de-vacuates all of them at once: GrothendieckGroup/CentralChargeK3.lean, CategoricalCharge.lean, RadicalKernel.lean, Realization.lean (the preservesEuler family and the two isometry constructions), EulerTransfer.lean and Walls/Spherical/Basic.lean.

The three coordinates #

mukaiVector is (rank, c₁, mukaiSInt) and mukaiSInt = χ − rank. On this model χ(E) = 2·E 0 + 2d·E 2 and rank E = E 0, so

v(E) = (E 0, E 1, E 0 + 2d·E 2)

which mukaiVector_k3 records. Two classes are worth naming: the structure sheaf ![1,0,0] has v = (1,0,1) and is spherical, and the point class ![0,0,1] has v = (0,0,2d) and is isotropic. Those are the two distinguished classes of Mukai/Basic.lean, inhabited here for the first time.

`d ≠ 0` is needed less often than expected #

The Mukai-vector computations below are evaluations on the model, not consequences of Riemann–Roch, so they hold for every d — including d = 0, where the "K3" is degenerate. Only mukaiPairing_k3, which crosses to mukaiPairing through pairing_mukaiVector, needs SatisfiesHRR and IsK3 and hence d ≠ 0. Carrying hd on the others would be a hypothesis nothing uses.

Main results #

k3MukaiForm, k3IntegralMukaiData, k3AdditiveMukaiData — the witnesses.
mukaiVector_k3 and pairing_mukaiVector_k3 — the coordinates and the pairing, evaluated.
mukaiPairing_k3 — the bridge to mukaiPairing, where d ≠ 0 is spent.
isSpherical_structureSheaf_k3, isIsotropic_point_k3.

The form and the data #

source

def AlgebraicGeometry.Numerical.Examples.k3MukaiForm (d : ℕ) :

ℤ →ₗ[ℤ ] ℤ →ₗ[ℤ ] ℤ

The Mukai form of the degree-2d model on Λ = ℤ: ⟪x, y⟫ = 2d·x·y.

This is the intersection form of the rank-one Néron–Severi lattice ℤ·H with ∫H² = 2d, which is what b_spec has to reproduce.

Equations

AlgebraicGeometry.Numerical.Examples.k3MukaiForm d = LinearMap.mk₂ ℤ (fun (x y : ℤ) => 2 * ↑d * x * y) ⋯ ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.k3MukaiForm_apply (d : ℕ) (x y : ℤ) :

((k3MukaiForm d) x) y = 2 * ↑d * x * y

source

noncomputable def AlgebraicGeometry.Numerical.Examples.k3IntegralMukaiData (d : ℕ) :

K3.IntegralMukaiData (k3NumericalVariety d) ℤ

The first IntegralMukaiData in the repository.

b_spec is the whole content: the integral form must compute the intersection number of first Chern classes. On this model ch₁(E) = (E 1)·H, so the product is (E 1)(F 1)·H² and its degree is 2d·(E 1)(F 1).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def AlgebraicGeometry.Numerical.Examples.k3AdditiveMukaiData (d : ℕ) :

K3.AdditiveMukaiData (k3NumericalVariety d) ℤ

The same data with additivity of c₁, which on SurfaceNum = Fin 3 → ℤ is pointwise addition and therefore rfl.

Equations

AlgebraicGeometry.Numerical.Examples.k3AdditiveMukaiData d = { toIntegralMukaiData := AlgebraicGeometry.Numerical.Examples.k3IntegralMukaiData d, c₁_add := ⋯ }

Instances For

The coordinates, evaluated #

source

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.mukaiVector_k3 (d : ℕ) (E : SurfaceNum) :

(k3IntegralMukaiData d).mukaiVector E = (E 0, E 1, E 0 + 2 * ↑d * E 2)

The Mukai vector on the model: v(E) = (E 0, E 1, E 0 + 2d·E 2).

The third coordinate is χ − rank, and χ(E) = 2·E 0 + 2d·E 2 on this presentation.

source

theorem AlgebraicGeometry.Numerical.Examples.pairing_mukaiVector_k3 (d : ℕ) (E F : SurfaceNum) :

Mukai.pairing (k3MukaiForm d) ((k3IntegralMukaiData d).mukaiVector E) ((k3IntegralMukaiData d).mukaiVector F) = 2 * ↑d * E 1 * F 1 - E 0 * (F 0 + 2 * ↑d * F 2) - F 0 * (E 0 + 2 * ↑d * E 2)

The Mukai pairing on the model, written out: ⟪v(E), v(F)⟫ = 2d·(E 1)(F 1) − (E 0)·s(F) − (F 0)·s(E) with s(E) = E 0 + 2d·E 2.

An evaluation, not a consequence of Riemann–Roch — hence no d ≠ 0.

source

theorem AlgebraicGeometry.Numerical.Examples.mukaiPairing_k3 (d : ℕ) (hd : d ≠ 0) (E F : SurfaceNum) :

↑(2 * ↑d * E 1 * F 1 - E 0 * (F 0 + 2 * ↑d * F 2) - F 0 * (E 0 + 2 * ↑d * E 2)) = K3.mukaiPairing (k3NumericalVariety d) E F

The bridge to mukaiPairing. This is the one statement here that crosses from the lattice to the numerical pairing, so it is the one that spends SatisfiesHRR and IsK3 — and hence d ≠ 0.