The numerical intersection ring generated by one ample class, in every dimension #

The hypothesis is that the whole numerical intersection ring A^•(X)_ℚ is generated, as a ℚ-algebra, by a single ample class H. Then it is ℚ[t]/(t^{n+1}) with t = H, graded by codimension, and the degree map is pinned by where it sends Hⁿ.

Picard rank one is not that hypothesis above dimension two. Models/Surface/RankOne.lean builds the n = 2 case from Pic X = ℤ·H, and there the two agree: a surface has A^0 = A^2 = ℚ and A^1 = ℚ·H, so H² ≠ 0 already generates everything. For n ≥ 3 the rank of N¹(X) says nothing about N²(X), which can be larger than ℚ·H²; the generated-by-H assumption is strictly stronger and is the one every construction below actually uses. A model built here is therefore not licensed by exhibiting a variety of Picard rank one.

The rankOne prefix on the declarations is historical and names the n = 2 case it was extracted from; it is not a claim that Picard rank one suffices.

This file does the construction once, for arbitrary n, and hands back a constructor for NumericalVarietyData. A model then costs exactly four numbers-worth of input: the degree ∫_X Hⁿ, the Chern-character coefficients of a class, the Todd coefficients of X, and the Euler characteristic — plus one rational identity relating them.

Main definitions #

RankOneRing n — the ring ℚ[t]/(t^{n+1}).
rankOneH n — the ample generator H, the image of t.
rankOneDegree n d — ∫_X, normalised by ∫_X Hⁿ = d.
rankOneNumericalRing n d — the NumericalRingData n structure.
rankOneNumericalVariety — the NumericalVarietyData n constructor.

Main results #

rankOneDegree_pow — ∫_X Hᵏ is d when k = n and 0 otherwise, including for k > n, where the power itself vanishes.
rankOneDegree_sum_mul_sum — the Riemann–Roch integral ∫_X (Σᵢ cᵢHⁱ)(Σⱼ tⱼHʲ) = d · Σᵢ cᵢ·t_{n−i}.

Implementation notes #

Chern and Todd components are defined without a case split on i ≤ n: the component in codimension i is algebraMap (coefficient i) * Hⁱ for every i, and above the dimension Hⁱ = 0 makes it vanish on its own. That removes an if from every downstream membership proof, at the cost of the caller's coefficient function being ignored above the dimension.

The existing surface construction is not rebuilt on top of this file. SurfaceRing is the n = 2 case of RankOneRing, but migrating Models/Surface/K3.lean and Models/Surface/ProjectivePlane.lean onto the general ring would rewrite two working models and their audit entries for no new mathematics; it is deliberate follow-up work, not part of this file.

d is a rational rather than a natural because a model may want a normalisation that is not the self-intersection of an integral class. The individual models take integer degrees.

References #

Hartshorne, Algebraic Geometry, appendix A
Fulton, Intersection Theory, ch. 15 and 19

The numerical intersection ring generated by one ample class, in every dimension #

Main definitions #

Main results #

Implementation notes #

References #

The ring ℚ[t]/(t^{n+1}) #

The grading by codimension #

The degree map, pinned by ∫_X Hⁿ = d #

Chern character, Todd class, and the variety constructor #

The ring `ℚ[t]/(t^{n+1})` #

The degree map, pinned by `∫_X Hⁿ = d` #