The numerical model of ℙ⁴

The first model of NumericalVarietyData in dimension four, and the one that exercises every term of Fourfold.chi_eq: all five Todd coefficients of ℙ⁴ are nonzero, so no term is multiplied by zero and an error anywhere in the display formula is visible here.

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

td(ℙ⁴) = 1 + (5/2)H + (35/12)H² + (25/12)H³ + H⁴,

from c₁ = 5H and c₂ = 10H²: td₁ = c₁/2, td₂ = (c₁² + c₂)/12 = (25 + 10)/12, td₃ = c₁c₂/24 = 50/24, and td₄ normalised by χ(O) = 1.

Main definitions

• p4NumericalVariety — the model.

Main results

• p4ChiStructureSheaf — ∫_{ℙ⁴} td₄ = χ(O_{ℙ⁴}) = 1.
• p4Chi_lineBundle — Riemann–Roch on this model reproduces χ(O(m)) = (m+1)(m+2)(m+3)(m+4)/24.
• p4ChCoeff_lineBundle_four — the class used there really is O(m): its Chern character is e^{mH} in codimension four, which is the only check on the 7/12 and −3/2 of Models/Fourfold/LinearSection.lean.

def AlgebraicGeometry.Numerical.Examples.p4Todd : ℕ → ℚ

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

Equations

• AlgebraicGeometry.Numerical.Examples.p4Todd 0 = 1
• AlgebraicGeometry.Numerical.Examples.p4Todd 1 = 5 / 2
• AlgebraicGeometry.Numerical.Examples.p4Todd 2 = 35 / 12
• AlgebraicGeometry.Numerical.Examples.p4Todd 3 = 25 / 12
• AlgebraicGeometry.Numerical.Examples.p4Todd 4 = 1
• AlgebraicGeometry.Numerical.Examples.p4Todd n.succ.succ.succ.succ.succ = 0

def AlgebraicGeometry.Numerical.Examples.p4Chi : FourfoldNum →+ ℤ

The Euler characteristic on ℙ⁴ in linear-section coordinates. Every generator is the structure sheaf of a linear subspace, with χ(O_{ℙᵏ}) = 1, so χ is the sum of the coordinates.

Equations

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

@[reducible]

noncomputable def AlgebraicGeometry.Numerical.Examples.p4NumericalVariety : NumericalVarietyData 4 (RankOneRing 4) FourfoldNum

The model. ℙ⁴, with ∫H⁴ = 1 and td = 1 + (5/2)H + (35/12)H² + (25/12)H³ + H⁴.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.p4NumericalVariety_satisfiesHRR : p4NumericalVariety.SatisfiesHRR

The explicit projective-four-space presentation satisfies HRR.

theorem AlgebraicGeometry.Numerical.Examples.p4ChiStructureSheaf : Fourfold.chiStructureSheaf p4NumericalVariety = 1

∫_{ℙ⁴} td₄ = χ(O_{ℙ⁴}) = 1.

theorem AlgebraicGeometry.Numerical.Examples.p4Chi_lineBundle (m c e f : ℤ) (hc : 2 * c = m * (m + 1)) (he : 6 * e = m * (m + 1) * (m + 2)) (hf : 24 * f = m * (m + 1) * (m + 2) * (m + 3)) : 24 * p4Chi ![1, m, c, e, f] = (m + 1) * (m + 2) * (m + 3) * (m + 4)

Riemann–Roch on ℙ⁴ reproduces χ(O(m)) = (m+1)(m+2)(m+3)(m+4)/24.

O(mH) is the class (1, m, c, e, f) whose coordinates are the binomial coefficients C(m+1,2), C(m+2,3) and C(m+3,4); the hypotheses state them cleared of denominators, so the class is integral for every m.

theorem AlgebraicGeometry.Numerical.Examples.p4ChCoeff_lineBundle_four (m c e f : ℤ) (hc : 2 * c = m * (m + 1)) (he : 6 * e = m * (m + 1) * (m + 2)) (hf : 24 * f = m * (m + 1) * (m + 2) * (m + 3)) : fourfoldChCoeff 1 ![1, m, c, e, f] 4 = ↑m ^ 4 / 24

The class of p4Chi_lineBundle really has ch₄ = m⁴/24, the top Chern-character component of e^{mH}. This is the coefficient the 7/12 and −3/2 of Models/Fourfold/LinearSection.lean feed into, so it is where a transcription error in those numbers would surface.