The intersection ring of a Picard-rank-one surface

Every smooth projective surface with Pic X = ℤ·H has the same numerical intersection ring up to the one number ∫_X H²: it is ℚ[t]/(t³) with t = H, graded by codimension, and the degree map is pinned by where it sends H².

So the ring, its grading, the Chern character in the basis 1, H, H², and the degree map on the normal form are all shared. What distinguishes one surface from another is only the Todd class, and that is what the individual model files supply:

• Models/Surface/K3.lean — td = 1 + 0 + (1/d)H² on a K3 of degree H² = 2d;
• Models/Surface/ProjectivePlane.lean — td = 1 + (3/2)H + H² on ℙ², where H² = 1;
• Models/Surface/Abelian.lean — td = 1 + 0 + 0 on an abelian surface.

The degree is parametrised by h2 = ∫_X H² rather than by a surface, so a new Picard-rank-one model costs a Todd class and nothing else.

Models/MonogenicRing.lean performs this same construction in arbitrary dimension, and the threefold and fourfold models are built on it. This file is not rebuilt on top of that one: see the implementation notes there for why.

The ring ℚ[t]/(t³)

noncomputable def AlgebraicGeometry.Numerical.Examples.surfaceRel : Polynomial ℚ

The defining relation: nothing survives in codimension three on a surface.

Equations

• AlgebraicGeometry.Numerical.Examples.surfaceRel = Polynomial.X ^ 3

theorem AlgebraicGeometry.Numerical.Examples.surfaceRel_ne_zero : surfaceRel ≠ 0

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.SurfaceRing : Type

The numerical intersection ring A^•(X)_ℚ = ℚ[t]/(t³).

Equations

• AlgebraicGeometry.Numerical.Examples.SurfaceRing = AdjoinRoot AlgebraicGeometry.Numerical.Examples.surfaceRel

noncomputable def AlgebraicGeometry.Numerical.Examples.surfacePB : PowerBasis ℚ SurfaceRing

The power basis 1, H, H².

Equations

• AlgebraicGeometry.Numerical.Examples.surfacePB = AdjoinRoot.powerBasis AlgebraicGeometry.Numerical.Examples.surfaceRel_ne_zero

theorem AlgebraicGeometry.Numerical.Examples.surfacePB_dim : surfacePB.dim = 3

noncomputable def AlgebraicGeometry.Numerical.Examples.H : SurfaceRing

The ample generator of the Picard group.

Equations

• AlgebraicGeometry.Numerical.Examples.H = AdjoinRoot.root AlgebraicGeometry.Numerical.Examples.surfaceRel

theorem AlgebraicGeometry.Numerical.Examples.surfacePB_gen : surfacePB.gen = H

theorem AlgebraicGeometry.Numerical.Examples.surfacePB_basis_apply (i : Fin surfacePB.dim) : surfacePB.basis i = H ^ ↑i

theorem AlgebraicGeometry.Numerical.Examples.H_pow_three : H ^ 3 = 0

H³ = 0: the relation, in the ring.

theorem AlgebraicGeometry.Numerical.Examples.H_pow_four : H ^ 4 = 0

def AlgebraicGeometry.Numerical.Examples.surfaceW : Fin surfacePB.dim → ℕ

The codimension of Hⁱ is i.

Equations

• AlgebraicGeometry.Numerical.Examples.surfaceW i = ↑i

theorem AlgebraicGeometry.Numerical.Examples.surfaceW_le (i : Fin surfacePB.dim) : surfaceW i ≤ 2

theorem AlgebraicGeometry.Numerical.Examples.two_lt_dim : 2 < surfacePB.dim

def AlgebraicGeometry.Numerical.Examples.idx2 : Fin surfacePB.dim

The index of H², the top graded piece.

Equations

• AlgebraicGeometry.Numerical.Examples.idx2 = ⟨2, AlgebraicGeometry.Numerical.Examples.two_lt_dim⟩

theorem AlgebraicGeometry.Numerical.Examples.surface_one_mem : 1 ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW 0

theorem AlgebraicGeometry.Numerical.Examples.surface_mul_mem (p q : Fin surfacePB.dim) : surfacePB.basis p * surfacePB.basis q ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW (surfaceW p + surfaceW q)

theorem AlgebraicGeometry.Numerical.Examples.H_mem_piece_one : H ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW 1

theorem AlgebraicGeometry.Numerical.Examples.Hsq_mem_piece_two : H ^ 2 ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW 2

theorem AlgebraicGeometry.Numerical.Examples.algebraMap_mul_mem {i : ℕ} {x : SurfaceRing} (q : ℚ) (hx : x ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW i) : (algebraMap ℚ SurfaceRing) q * x ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW i

The degree map, pinned by ∫_X H² = h2

noncomputable def AlgebraicGeometry.Numerical.Examples.surfaceDegree (h2 : ℚ) : SurfaceRing →ₗ[ℚ] ℚ

∫_X, normalised so that ∫_X H² = h2.

Equations

• AlgebraicGeometry.Numerical.Examples.surfaceDegree h2 = h2 • AlgebraicGeometry.Numerical.Examples.surfacePB.basis.coord AlgebraicGeometry.Numerical.Examples.idx2

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_basis_of_ne (h2 : ℚ) (i : Fin surfacePB.dim) (hi : surfaceW i ≠ 2) : (surfaceDegree h2) (surfacePB.basis i) = 0

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_basis_two (h2 : ℚ) : (surfaceDegree h2) (surfacePB.basis idx2) = h2

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_one (h2 : ℚ) : (surfaceDegree h2) 1 = 0

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_H (h2 : ℚ) : (surfaceDegree h2) H = 0

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_Hsq (h2 : ℚ) : (surfaceDegree h2) (H ^ 2) = h2

∫_X H² = h2: the degree of the surface.

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_algebraMap_mul (h2 q : ℚ) (x : SurfaceRing) : (surfaceDegree h2) ((algebraMap ℚ SurfaceRing) q * x) = q * (surfaceDegree h2) x

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_normalForm (h2 a b c : ℚ) : (surfaceDegree h2) ((algebraMap ℚ SurfaceRing) a + (algebraMap ℚ SurfaceRing) b * H + (algebraMap ℚ SurfaceRing) c * H ^ 2) = h2 * c

∫_X on the normal form a + b·H + c·H². Only the top coefficient survives.

@[reducible]

noncomputable def AlgebraicGeometry.Numerical.Examples.surfaceNumericalRing (h2 : ℚ) : NumericalRingData 2 SurfaceRing

The numerical intersection ring of a Picard-rank-one surface with ∫_X H² = h2.

Equations

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

The Chern character

All three models use the same N. K3.lean and Abelian.lean share k3ChCoeff; ProjectivePlane.lean reparametrises with its own p2ChCoeff, because ch₂ is a half-integer on ℙ² — see Models/Surface/ProjectivePlane.lean. Coefficients are therefore rational rather than integral.

@[reducible, inline]

abbrev AlgebraicGeometry.Numerical.Examples.SurfaceNum : Type

A class is recorded by the three rational coefficients of ch = a + b·H + c·H².

Equations

• AlgebraicGeometry.Numerical.Examples.SurfaceNum = (Fin 3 → ℤ)

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

Shared Chern-character coordinates for the rank-one surface models: the class (r, c, s) has ch = r + c·H + s·H².

The historical name is retained even though the construction is not K3-specific.

Equations

• AlgebraicGeometry.Numerical.Examples.k3ChCoeff E 0 = ↑(E 0)
• AlgebraicGeometry.Numerical.Examples.k3ChCoeff E 1 = ↑(E 1)
• AlgebraicGeometry.Numerical.Examples.k3ChCoeff E 2 = ↑(E 2)
• AlgebraicGeometry.Numerical.Examples.k3ChCoeff E n.succ.succ.succ = 0

theorem AlgebraicGeometry.Numerical.Examples.k3ChCoeff_add (E F : SurfaceNum) (i : ℕ) : k3ChCoeff (E + F) i = k3ChCoeff E i + k3ChCoeff F i

noncomputable def AlgebraicGeometry.Numerical.Examples.surfaceCh (chCoeff : SurfaceNum → ℕ → ℚ) (E : SurfaceNum) : ℕ → SurfaceRing

The Chern character of E, given its coefficient functions. chCoeff E i is the coefficient of Hⁱ; keeping it abstract lets ℙ² use half-integers.

Equations

• AlgebraicGeometry.Numerical.Examples.surfaceCh chCoeff E 0 = (algebraMap ℚ AlgebraicGeometry.Numerical.Examples.SurfaceRing) (chCoeff E 0)
• AlgebraicGeometry.Numerical.Examples.surfaceCh chCoeff E 1 = (algebraMap ℚ AlgebraicGeometry.Numerical.Examples.SurfaceRing) (chCoeff E 1) * AlgebraicGeometry.Numerical.Examples.H
• AlgebraicGeometry.Numerical.Examples.surfaceCh chCoeff E 2 = (algebraMap ℚ AlgebraicGeometry.Numerical.Examples.SurfaceRing) (chCoeff E 2) * AlgebraicGeometry.Numerical.Examples.H ^ 2
• AlgebraicGeometry.Numerical.Examples.surfaceCh chCoeff E n.succ.succ.succ = 0

theorem AlgebraicGeometry.Numerical.Examples.surfaceCh_mem (chCoeff : SurfaceNum → ℕ → ℚ) (E : SurfaceNum) (i : ℕ) : surfaceCh chCoeff E i ∈ DerivedAlgGeo.LinearAlgebra.gradedPiece (⇑surfacePB.basis) surfaceW i

theorem AlgebraicGeometry.Numerical.Examples.surfaceCh_add (chCoeff : SurfaceNum → ℕ → ℚ) (hadd : ∀ (E F : SurfaceNum) (i : ℕ), chCoeff (E + F) i = chCoeff E i + chCoeff F i) (E F : SurfaceNum) (i : ℕ) : surfaceCh chCoeff (E + F) i = surfaceCh chCoeff E i + surfaceCh chCoeff F i

theorem AlgebraicGeometry.Numerical.Examples.surfaceCh_sum (chCoeff : SurfaceNum → ℕ → ℚ) (E : SurfaceNum) : ∑ i ∈ Finset.range (2 + 1), surfaceCh chCoeff E i = (algebraMap ℚ SurfaceRing) (chCoeff E 0) + (algebraMap ℚ SurfaceRing) (chCoeff E 1) * H + (algebraMap ℚ SurfaceRing) (chCoeff E 2) * H ^ 2

theorem AlgebraicGeometry.Numerical.Examples.surfaceDegree_ch_mul_todd (h2 a b c t₁ t₂ : ℚ) : (surfaceDegree h2) (((algebraMap ℚ SurfaceRing) a + (algebraMap ℚ SurfaceRing) b * H + (algebraMap ℚ SurfaceRing) c * H ^ 2) * (1 + (algebraMap ℚ SurfaceRing) t₁ * H + (algebraMap ℚ SurfaceRing) t₂ * H ^ 2)) = h2 * (a * t₂ + b * t₁ + c)

The product ch(E)·td(X), reduced. Everything of codimension above two is killed by H³ = H⁴ = 0, leaving the codimension-two coefficient a·t₂ + b·t₁ + c.

This is the computational core shared by every Picard-rank-one model.