The slope API on the rank-one K3 model

noncomputable def AlgebraicGeometry.Numerical.Examples.k3Polarization (d : ℕ) (hd : d ≠ 0) : Polarization (surfaceNumericalRing (2 * ↑d))

The hyperplane class as a polarisation of the K3 numerical ring.

Equations

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

theorem AlgebraicGeometry.Numerical.Examples.degH_k3 (d : ℕ) (hd : d ≠ 0) (E : SurfaceNum) : degH (k3NumericalVariety d) (k3Polarization d hd) E = 2 * ↑d * ↑(E 1)

The H-degree on the K3 model is 2d times the ch₁ coefficient.