The polarised-surface transport is the compressed divisorial transport #
Walls/Divisorial/Circle.lean shows that fixing the transverse parameter of a
divisorial slice gives exactly the (s,t) model, pulled back along the
degree-weighted triple ChargeCoordinates.toNumClass. This file records the
one statement in that comparison whose type mentions a numerical variety: the
transport Surface.toNumClass of WallTransport.lean is that triple, read off
the coordinates ofNumericalData extracts. The two differ only by where the
rational-to-real cast of the product ∫H² · rank is taken.
theorem
AlgebraicGeometry.Numerical.Surface.toNumClass_eq_ofNumericalData
{A : Type u}
{N : Type v}
[CommRing A]
[Algebra ℚ A]
[AddCommGroup N]
(V : NumericalVarietyData 2 A N)
(P : Polarization V.ring)
(E : N)
:
The polarised-surface transport of WallTransport.lean is the compressed
transport of the coordinates it reads off. The two differ only by where the
rational-to-real cast of the product ∫H² · rank is taken.