Principal divisors on a Weierstrass curve have degree zero #
Theorem statement: WeierstrassCurve.Affine.hasPrincipalDivisors_functionField
(c0f259e5-85a4-5e9a-bc15-621436aa0746), by Claude, 2026-09-05.
Proof: submission 71997f8e-42a1-5c8d-8da4-f9d0556bcf71, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ be a field of characteristic $0$ and let $W$ be an affine Weierstrass curve over $F$, with
function field $F(W) =$ W.FunctionField. The assertion is that $F(W)$, viewed as an extension of
$F$, satisfies the class
AlgebraicCurve.HasPrincipalDivisors: for every
$f \in F(W)$ with $f \neq 0$ there is a divisor $D$, that is, a finitely supported function from the
places of $F(W)/F$ to $\mathbb{Z}$, such that $D(v) = \operatorname{ord}_v(f)$ for every place $v$,
and such that $\deg D = 0$. Here a place of $F(W)/F$ is a valuation subring $\mathcal{O}_v \subseteq F(W)$ which contains the image of $F$ under the structure map, is not the whole of $F(W)$, and is a
principal ideal ring; $\deg D$ is the integer $\sum_v D(v)\,\deg v$, obtained from $D$ by summing
its values weighted by the residue degrees $\deg v$. Thus the statement packages two facts at once:
a nonzero $f$ has $\operatorname{ord}_v(f) = 0$ for all but finitely many places (so that the
prescribed function is indeed finitely supported), and the resulting divisor of $f$ has degree zero.
No smoothness or nonsingularity hypothesis is imposed on $W$.
This is the degree-zero theorem for principal divisors, in the form needed for the function field of
a plane Weierstrass model: $F(W)$ is a finite extension of the rational function field $F(x)$,
generated by $y$ satisfying the monic Weierstrass quadratic, so the general result for finite
extensions of $F(x)$ applies. It supplies the HasPrincipalDivisors instance used throughout the
divisor-class-group layer, in particular in the analysis of modular polynomials and Vélu quotients.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_Affine_hasPrincipalDivisors_functionField.lean
<!-- Generated by add_prove2me_provenance.py -->