Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Models.Surface.Abelian

A polarised abelian surface #

The third surface model, and the degenerate one: on an abelian surface c₁ = c₂ = 0, so

td(A) = 1 + 0 + 0

and Riemann–Roch collapses to χ(E) = ∫_A ch₂(E). Both other terms of Surface.chi_eq vanish, and they vanish for different reasons than on a K3 — there ∫td₂ = 2 keeps the rank term alive, here it is 0.

That makes this the surface model where χ sees neither the rank nor c₁, which is the two-dimensional shadow of CalabiYauThreefold.chi_eq_of_chComp_eq. It is worth having for exactly that reason: a Bridgeland central charge normalised against χ degenerates here in a way it does not on a K3, and a statement that silently assumed ∫td₂ ≠ 0 would pass on both other surface models.

A carries a polarisation H of type (1, d), so ∫_A H² = 2d. The evenness is an input, not something this model checks: it is Riemann–Roch on A itself — χ(O_A(H)) = H²/2 must be an integer — and [O_A(H)] is one of the classes the integral lattice SurfaceNum below does not contain, so the model cannot evaluate it.

Chern-character coordinates #

These are the same as the K3's — a class (r, c, s) has ch = r + c·H + s·H² in the basis 1, H, H² — so k3ChCoeff is reused rather than copied. That is the design Models/Surface/RankOne.lean states outright: within Picard rank one, a new model costs a Todd class and nothing else.

s ranging over ℤ makes N the sublattice of classes whose ch₂ is an integer multiple of H², which is a genuine restriction — O(mH) has ch₂ = (m²/2)H² and so lies in it only for even m. The K3 model carries the same restriction and for the same reason; where a model needs the full lattice it must reparametrise, as Models/Surface/ProjectivePlane.lean does.

Main definitions #

Main results #

source
noncomputable def AlgebraicGeometry.Numerical.Examples.abelianTodd :
ℕ → SurfaceRing

The Todd class of an abelian surface: c₁ = c₂ = 0, so every component above td₀ vanishes.

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

    The model. An abelian surface with a polarisation of type (1, d), so ∫_A H² = 2d, and trivial Todd class.

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

      With trivial Todd class, HRR reduces to the top Chern-character coordinate multiplied by the polarization degree 2d.

      source
      theorem AlgebraicGeometry.Numerical.Examples.abelianToddComp_one (d : ℕ) :
      (abelianNumericalVariety d).toddComp 1 = 0

      td₁ = 0: the canonical class of an abelian surface is trivial.

      source
      theorem AlgebraicGeometry.Numerical.Examples.abelianChiStructureSheaf (d : ℕ) :
      Surface.chiStructureSheaf (abelianNumericalVariety d) = 0

      ∫_A td₂ = χ(O_A) = 0. Together with abelianToddComp_one this is the abelian-surface analogue of k3_isK3, stated as two theorems because — unlike K3s and Calabi–Yau threefolds — abelian surfaces have no class in this library to inhabit.

      source
      theorem AlgebraicGeometry.Numerical.Examples.abelianChi_eq_of_chComp_two_eq (d : ℕ) (E F : SurfaceNum) (h : (abelianNumericalVariety d).chComp E 2 = (abelianNumericalVariety d).chComp F 2) :
      (abelianNumericalVariety d).chi E = (abelianNumericalVariety d).chi F

      On an abelian surface χ sees neither the rank nor c₁: two classes agreeing in codimension two have the same Euler characteristic, however their ranks and first Chern classes differ.

      This is the two-dimensional shadow of CalabiYauThreefold.chi_eq_of_chComp_eq, and it is the reason to carry this model alongside the K3: on a K3 the rank term survives with coefficient ∫td₂ = 2, so the same statement is false there.