Documentation

DerivedAlgGeo.AlgebraicGeometry.Numerical.Models.Threefold.ProjectiveSpace

The numerical model of ℙ³ #

The first model of NumericalVarietyData in dimension three. Before it, every statement in DerivedAlgGeo/AlgebraicGeometry/Numerical/Specializations/Threefold.lean was conditional on a NumericalVarietyData 3 A N existing at all.

ℙ³ is the threefold analogue of Models/Surface/ProjectivePlane.lean, and it is here for the same reason: every Todd coefficient is nonzero, so it is the model that can detect a sign or index error anywhere in Threefold.chi_eq. A Calabi–Yau model cannot — two of the four terms are multiplied by zero there.

The data: Pic ℙ³ = ℤ·H with ∫H³ = 1, and

td(ℙ³) = 1 + 2H + (11/6)H² + H³,

whose components are td₁ = −K/2 = 2H from K = −4H, td₂ = (c₁² + c₂)/12 = (16 + 6)/12, and td₃ = c₁c₂/24 = 24/24 = 1, giving χ(O) = 1.

Main definitions #

Main results #

source
def AlgebraicGeometry.Numerical.Examples.p3Todd :
ℕ → ℚ

The Todd coefficients of ℙ³ against the powers of H.

Equations
Instances For
    source
    def AlgebraicGeometry.Numerical.Examples.p3Chi :
    ThreefoldNum →+ ℤ

    The Euler characteristic on ℙ³ in linear-section coordinates.

    Every generator is the structure sheaf of a linear subspace, and χ(O_{ℙᵏ}) = 1 for each of them, so χ is the plain sum of the coordinates. That this agrees with Riemann–Roch is the hchi obligation discharged in p3NumericalVariety.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible]
      noncomputable def AlgebraicGeometry.Numerical.Examples.p3NumericalVariety :
      NumericalVarietyData 3 (RankOneRing 3) ThreefoldNum

      The model. ℙ³, with ∫H³ = 1 and td = 1 + 2H + (11/6)H² + H³.

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

        The explicit projective-three-space presentation satisfies HRR.

        source
        theorem AlgebraicGeometry.Numerical.Examples.p3ChiStructureSheaf :
        Threefold.chiStructureSheaf p3NumericalVariety = 1

        ∫_{ℙ³} td₃ = χ(O_{ℙ³}) = 1.

        source
        theorem AlgebraicGeometry.Numerical.Examples.p3Chi_lineBundle (m c e : ℤ) (hc : 2 * c = m * (m + 1)) (he : 6 * e = m * (m + 1) * (m + 2)) :
        6 * p3Chi ![1, m, c, e] = (m + 1) * (m + 2) * (m + 3)

        Riemann–Roch on ℙ³ reproduces χ(O(m)) = (m+1)(m+2)(m+3)/6.

        O(mH) is the class (1, m, c, e) with 2c = m(m+1) and 6e = m(m+1)(m+2); those are the binomial coefficients C(m+1,2) and C(m+2,3), so the class is integral for every m, including negative m. Stated cleared of denominators to stay in ℤ.

        source
        theorem AlgebraicGeometry.Numerical.Examples.p3ChCoeff_lineBundle_two (m c e : ℤ) (hc : 2 * c = m * (m + 1)) :
        threefoldChCoeff 1 ![1, m, c, e] 2 = ↑m ^ 2 / 2

        The class of p3Chi_lineBundle really has ch₂ = m²/2. Without this and its codimension-three companion, p3Chi_lineBundle would only be arithmetic about a quadruple.

        source
        theorem AlgebraicGeometry.Numerical.Examples.p3ChCoeff_lineBundle_three (m c e : ℤ) (hc : 2 * c = m * (m + 1)) (he : 6 * e = m * (m + 1) * (m + 2)) :
        threefoldChCoeff 1 ![1, m, c, e] 3 = ↑m ^ 3 / 6

        The class of p3Chi_lineBundle really has ch₃ = m³/6.