Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Models.Surface.K3

A K3 surface of Picard rank one #

The first model of NumericalVarietyData in dimension two. Before it, every statement in DerivedAlgGeo/AlgebraicGeometry/Numerical/Specializations/Surface.lean and DerivedAlgGeo/AlgebraicGeometry/Numerical/RiemannRoch/K3.lean was conditional on a NumericalVarietyData 2 A N existing at all — only the dimension-zero point had been exhibited.

The surface is a K3 X with Pic X = ℤ·H and H² = 2d. The ring, grading and degree map come from Numerical/Models/Surface/RankOne.lean; all this file supplies is the Todd class

td(X) = 1 + 0 + (1/d)·H²,

so that td₁ = 0 and ∫_X td₂ = 2 — which is exactly K3.IsK3, proved here rather than assumed.

d is a parameter, not fixed to 1: the Bridgeland wall structure on a K3 depends on the degree. It is a natural number rather than a rational because χ must land in ℤ — Riemann–Roch on this model reads χ(r, c, s) = 2r + 2ds.

source
noncomputable def AlgebraicGeometry.Numerical.Examples.k3Todd (d : ℚ) :
ℕ → SurfaceRing

The Todd class of a K3: td₁ = 0, and td₂ normalised so that ∫_X td₂ = 2.

Equations
Instances For
    source
    theorem AlgebraicGeometry.Numerical.Examples.k3Todd_mem (d : ℚ) (i : ℕ) :
    k3Todd d i ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW i
    source
    theorem AlgebraicGeometry.Numerical.Examples.k3Todd_sum (d : ℚ) :
    ∑ j ∈ Finset.range (2 + 1), k3Todd d j = 1 + (algebraMap ℚ SurfaceRing) 0 * H + (algebraMap ℚ SurfaceRing) (1 / d) * H ^ 2
    source
    @[reducible]
    noncomputable def AlgebraicGeometry.Numerical.Examples.k3NumericalVariety (d : ℕ) :
    NumericalVarietyData 2 SurfaceRing SurfaceNum

    The model. A K3 surface of degree H² = 2d, d > 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem AlgebraicGeometry.Numerical.Examples.k3NumericalVariety_satisfiesHRR (d : ℕ) (hd : d ≠ 0) :
      (k3NumericalVariety d).SatisfiesHRR

      The explicit K3 presentation satisfies Hirzebruch--Riemann--Roch.

      source
      theorem AlgebraicGeometry.Numerical.Examples.k3_isK3 (d : ℕ) (hd : d ≠ 0) :
      K3.IsK3 (k3NumericalVariety d)

      The model really is a K3: td₁ = 0 and ∫_X td₂ = χ(O_X) = 2.

      With this presentation and its two property witnesses, every theorem in DerivedAlgGeo/AlgebraicGeometry/Numerical/RiemannRoch/K3.lean — Riemann–Roch, the Mukai self-pairing, ⟨v,v⟩ = ∫Δ − 2r² — is a statement about an object that exists.

      source
      theorem AlgebraicGeometry.Numerical.Examples.k3ChiStructureSheaf (d : ℕ) (hd : d ≠ 0) :
      Surface.chiStructureSheaf (k3NumericalVariety d) = 2

      ∫_X td₂ = χ(O_X) = 2, in chiStructureSheaf form. The number is the one k3_isK3.degree_toddComp_two already carries — chiStructureSheaf unfolds to degree (toddComp 2) — so this is a projection, not a second computation. It exists so the rank-one surface models can be compared through one function.