Linear-section coordinates on a Picard-rank-one fourfold

The dimension-four counterpart of Models/Threefold/LinearSection.lean, with the same justification: a class is recorded by its multiplicities against

[O_X], [O_{X∩H}], [O_{X∩H²}], [O_{X∩H³}], [O_pt],

and ch(O_{X∩Hᵏ}) = (1 − e^{−H})ᵏ by the Koszul resolution. Expanding through codimension four:

• k = 1: H − H²/2 + H³/6 − H⁴/24
• k = 2: H² − H³ + (7/12)H⁴
• k = 3: H³ − (3/2)H⁴
• k = 4: H⁴, and a point is H⁴/d because ∫_X H⁴ = d.

The 7/12 and −3/2 are the terms that make dimension four more than a longer version of dimension three: they are the first coefficients of (1 − e^{−H})ᵏ that are neither ±1 nor a reciprocal factorial, so a model that got them wrong would still produce integral χ on three of its five generators.

Main definitions

• FourfoldNum — the coordinates (a, b, c, e, f).
• fourfoldChCoeff — the Chern-character coefficients on a fourfold of degree d.

Main results

• fourfoldChCoeff_add — additivity.
• fourfoldChi_sum — the Riemann–Roch sum with Finset.range 5 expanded.

References

• Hartshorne, Algebraic Geometry, I.7 and V.1
• Griffiths–Harris, Principles of Algebraic Geometry, ch. 4

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.FourfoldNum : Type

A class on a Picard-rank-one fourfold, in linear-section coordinates: (a, b, c, e, f) stands for a·[O_X] + b·[O_{X∩H}] + c·[O_{X∩H²}] + e·[O_{X∩H³}] + f·[O_pt].

Equations

• AlgebraicGeometry.Numerical.Examples.FourfoldNum = (Fin 5 → ℤ)

noncomputable def AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff (d : ℚ) (E : FourfoldNum) : ℕ → ℚ

The Chern-character coefficients of a class in linear-section coordinates on a fourfold of degree ∫_X H⁴ = d. The coefficient of Hⁱ is entry i. The 7/12 and −3/2 in entries 4 and 3 are the terms that do not follow the threefold pattern; see the module docstring for the expansion of (1 − e^{−H})ᵏ they come from.

Equations

• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E 0 = ↑(E 0)
• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E 1 = ↑(E 1)
• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E 2 = -↑(E 1) / 2 + ↑(E 2)
• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E 3 = ↑(E 1) / 6 - ↑(E 2) + ↑(E 3)
• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E 4 = -↑(E 1) / 24 + 7 * ↑(E 2) / 12 - 3 * ↑(E 3) / 2 + ↑(E 4) / d
• AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff d E n.succ.succ.succ.succ.succ = 0

theorem AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff_add (d : ℚ) (E F : FourfoldNum) (i : ℕ) : fourfoldChCoeff d (E + F) i = fourfoldChCoeff d E i + fourfoldChCoeff d F i

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

The rank of a class in linear-section coordinates is its [O_X] multiplicity: the other four generators are supported in positive codimension.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.fourfoldChCoeff_zero (d : ℚ) (E : FourfoldNum) : fourfoldChCoeff d E 0 = ↑(fourfoldRank E)

theorem AlgebraicGeometry.Numerical.Examples.fourfoldChi_sum (d : ℚ) (t : ℕ → ℚ) (E : FourfoldNum) : ∑ i ∈ Finset.range (4 + 1), fourfoldChCoeff d E i * t (4 - i) = ↑(E 0) * t 4 + ↑(E 1) * t 3 + (-↑(E 1) / 2 + ↑(E 2)) * t 2 + (↑(E 1) / 6 - ↑(E 2) + ↑(E 3)) * t 1 + (-↑(E 1) / 24 + 7 * ↑(E 2) / 12 - 3 * ↑(E 3) / 2 + ↑(E 4) / d) * t 0

The Riemann–Roch sum of rankOneNumericalVariety, with Finset.range 5 expanded and the 4 − i reductions performed.