Divisor of weilNum: simple zeros on the [n]-fibre over T #
Theorem statement: WeierstrassCurve.Affine.valuation_weilNum
(010cda30-3345-5c01-a0e7-6d0525ea9d06), by Claude, 2026-09-05.
Proof: submission 1a0848cc-b9b4-5d49-a82d-80181e2da33a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra and $K$ algebraically closed, let $W$ be a
Weierstrass curve over $F$ which is elliptic, and write $W⁄K$ for its base change, assumed to have
Dedekind affine coordinate ring $(W⁄K).\mathrm{CoordinateRing}$. Let $n$ be a natural number with
$(n : K) \neq 0$, let $T$ be a point of $W⁄K$ killed by $n$, i.e. $(n : \mathbb{Z}) \cdot T = 0$,
and let $P$ be a point of $W⁄K$ different from the point at infinity. The place placeOf W K P hP
is the height-one prime of the coordinate ring whose ideal is the ideal $\mathrm{XYIdeal}$ of the
affine coordinates $(P.\mathrm{xc}, P.\mathrm{yc})$ of $P$, maximal because those coordinates are
nonsingular, and nonzero because the class of $X$ is nonzero. The element weilNum W K n T is a
chosen generator of the ideal fibIdeal W K n T if that ideal is principal, and $1$ otherwise;
fibIdeal W K n T is the product of the ideals placeIdeal W K P over the members of fibSet W K n T, the fibre of $[n]$ over $T$, which is finite here, and is $\top$ if that set is infinite. The
assertion is that the valuation attached to placeOf W K P hP on the function field of $W⁄K$,
evaluated on the image of weilNum W K n T in the function field, equals $\exp(-1)$ when $(n : \mathbb{Z}) \cdot P = T$, and equals $1$ otherwise; that is, weilNum W K n T has a simple zero at
each point of the fibre of $[n]$ over $T$ and is a unit at every other affine point.
This is the divisor computation for the function whose divisor is $\sum_{nP = T} (P) - n^2 (O)$ used in the classical construction of the Weil pairing, as in Silverman III.8; the hypothesis that $T$ is $n$-torsion is what makes the fibre ideal principal, via the divisor-class criterion together with $\sum_{nP=T} P = 0$. It underlies the subsequent statements on valuations of Weil functions and on integral models of the Weil pairing over valuation subrings.
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_valuation_weilNum.lean
<!-- Generated by add_prove2me_provenance.py -->