Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Models.Surface.ProjectivePlane

The projective-plane numerical model #

A second model of NumericalVarietyData in dimension two, with a nontrivial canonical class.

That is the point of it. The K3 model has td₁ = 0, so the ∫_X c₁(E)·td₁(X) term of Surface.chi_eq is multiplied by zero there and a sign error in it would go undetected. On ℙ², K = −3H gives td₁ = −K/2 = (3/2)H, and the term carries weight.

The model: Pic ℙ² = ℤ·H with H² = 1, and

td(ℙ²) = 1 + (3/2)·H + H², so ∫ td₂ = χ(O_{ℙ²}) = 1.

The lattice #

ch₂ is a half-integer on ℙ²: ch₂ = (c₁² − 2c₂)/2, which is odd over two whenever c₁ is odd. So N cannot be ℤ³ with ch₂ as the third coordinate and still have χ land in ℤ. The numerical Grothendieck group is the sublattice where 3c₁ + 2ch₂ is even; substituting 2ch₂ = c₁ + 2v parametrises it by ℤ³ again, and this model uses those coordinates:

(r, c, v) ↦ ch = r + c·H + (c/2 + v)·H², χ = r + 2c + v.

The check that the parametrisation is right is p2Chi_lineBundle: it recovers χ(O(nH)) = (n+1)(n+2)/2.

source
noncomputable def AlgebraicGeometry.Numerical.Examples.p2ChCoeff (E : SurfaceNum) :
ℕ → ℚ

Chern-character coefficients on ℙ². The half-integer in codimension two is what forces the (r, c, v) coordinates — see the module docstring.

Equations
Instances For
    source
    theorem AlgebraicGeometry.Numerical.Examples.p2ChCoeff_add (E F : SurfaceNum) (i : ℕ) :
    p2ChCoeff (E + F) i = p2ChCoeff E i + p2ChCoeff F i
    source
    noncomputable def AlgebraicGeometry.Numerical.Examples.p2Todd :
    ℕ → SurfaceRing

    The Todd class of ℙ²: td₁ = −K/2 = (3/2)H and td₂ = H², so ∫ td₂ = χ(O) = 1.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Numerical.Examples.p2Todd_mem (i : ℕ) :
      p2Todd i ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW i
      source
      theorem AlgebraicGeometry.Numerical.Examples.p2Todd_sum :
      ∑ j ∈ Finset.range (2 + 1), p2Todd j = 1 + (algebraMap ℚ SurfaceRing) (3 / 2) * H + (algebraMap ℚ SurfaceRing) 1 * H ^ 2
      source
      theorem AlgebraicGeometry.Numerical.Examples.p2_chi_structureSheaf :
      (surfaceDegree 1) (p2Todd 2) = 1

      ∫_{ℙ²} td₂ = χ(O_{ℙ²}) = 1.

      source
      def AlgebraicGeometry.Numerical.Examples.p2Chi (E : SurfaceNum) :
      ℤ

      The Euler characteristic on ℙ², in the (r, c, v) coordinates.

      Equations
      Instances For
        source
        @[reducible]
        noncomputable def AlgebraicGeometry.Numerical.Examples.p2NumericalVariety :
        NumericalVarietyData 2 SurfaceRing SurfaceNum

        The model. ℙ², with H² = 1 and td = 1 + (3/2)H + H².

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem AlgebraicGeometry.Numerical.Examples.p2NumericalVariety_satisfiesHRR :
          p2NumericalVariety.SatisfiesHRR

          The explicit projective-plane presentation satisfies Hirzebruch--Riemann--Roch.

          source
          theorem AlgebraicGeometry.Numerical.Examples.p2Chi_lineBundle (n m : ℤ) (hm : 2 * m = n * (n - 1)) :
          2 * p2Chi ![1, n, m] = (n + 1) * (n + 2)

          Riemann–Roch on ℙ² reproduces χ(O(nH)) = (n+1)(n+2)/2.

          O(nH) is the class (1, n, m) with 2m = n(n−1): its Chern character is 1 + nH + (n²/2)H², and this model records ch₂ = c/2 + v. Stated doubled to stay in ℤ.

          This is the check that Surface.chi_eq's c₁·td₁ term is right — the K3 model, where td₁ = 0, cannot see it.

          source
          theorem AlgebraicGeometry.Numerical.Examples.p2ChCoeff_lineBundle (n m : ℤ) (hm : 2 * m = n * (n - 1)) :
          p2ChCoeff ![1, n, m] 2 = ↑n ^ 2 / 2

          The class (1, n, m) with 2m = n(n−1) really has ch₂ = n²/2, i.e. really is O(nH). Without this, p2Chi_lineBundle would only be arithmetic about a triple.