Isotropic 10-collections on an Enriques surface #

Li--Nuer--Stellari--Zhao, arXiv:1912.04332v2, Definition 3.2 and equation (3.2), attach to a Fano polarization Δ an isotropic 10-sequence of numerical classes fᵢ satisfying

3δ = f₁ + ⋯ + f₁₀.

This file records line-bundle lifts of those classes against a supplied surface intersection context. The repository has no geometric Num(Y) quotient, nef predicate, or ampleness API. Consequently the numerical equality is supplied in its intrinsic intersection-theoretic form: 3δ and ∑ fᵢ have equal intersection with every Picard class. The field does not claim that the chosen Picard lift is nef or ample, and no collection is constructed on a concrete surface.

The two arithmetic consequences used by the Torelli lane are proved rather than stored: Δ · Fᵢ = 3 and Δ² = 10. In particular, the stale value Δ · Fᵢ = 1 is not compatible with equation (3.2): the sum of the other nine isotropic classes pairs to 9.

Main definitions #

IsotropicCollection -- ten line bundles, a Fano-class lift, an intersection context, the isotropic equations, and the numerical normalization.
IsotropicCollection.classes and sumClass -- the additive Picard classes consumed by the lattice API.

Main results #

IsotropicCollection.isIsotropicSequence -- the geometric fields packaged at the generic lattice root.
IsotropicCollection.bundleClass_ne -- distinct indices give distinct Picard classes.
IsotropicCollection.fano_intersection_bundle -- Δ · Fᵢ = 3.
IsotropicCollection.fano_self_intersection -- Δ² = 10.

source

structure AlgebraicGeometry.EnriquesSurface.IsotropicCollection {k : Type u} [Field k] {Y : Scheme} [Y.Over (Spec (CommRingCat.of k))] [IsSmoothProperVariety k Y] {C : SmoothProperVariety.CanonicalSheafData k Y 2} [SmoothProperVariety.IsEnriquesSurface k Y C] (D : Cohomology.FiniteCohomology k Y) (S : D.LinearConnectingSystem) :

Type (u + 1)

Supplied geometric data for an isotropic 10-collection of line bundles.

The normalization is equation (3.2) of arXiv:1912.04332v2, expressed through all intersection probes because the repository does not yet construct Num(Y). fano is only a Picard lift of the numerical Fano class: nefness and ampleness are deliberately not asserted.

bundles : Fin 10 → Scheme.Modules.LineBundleData Y
The ten line-bundle lifts O_Y(Fᵢ).
fano : Scheme.Modules.LineBundleData Y
A line-bundle lift of the numerical class of the Fano polarization.
intersection : IntersectionTheory.Number.IntersectionContext D S 2
The supplied Snapper context in which all numerical equations are evaluated.
self_isotropic (i : Fin 10) : self.intersection.picardIntersectionNumber ![(self.bundles i).toPic, (self.bundles i).toPic] = 0
Each selected class is isotropic.
pairwise_one (i j : Fin 10) : i ≠ j → self.intersection.picardIntersectionNumber ![(self.bundles i).toPic, (self.bundles j).toPic] = 1
Distinct selected classes have intersection one.
fano_normalization (L : Scheme.Modules.Pic Y) : (self.intersection.surfaceIntersectionPairing (3 • Additive.ofMul self.fano.toPic)) (Additive.ofMul L) = (self.intersection.surfaceIntersectionPairing (∑ i : Fin 10, Additive.ofMul (self.bundles i).toPic)) (Additive.ofMul L)
Equation (3.2), 3δ = ∑ fᵢ, as numerical equivalence: both sides pair equally with every Picard class. This is supplied data because no Num(Y) quotient exists at the current pin.