Valuation of the Weil function g_T at an affine place #
Theorem statement: WeierstrassCurve.Affine.valuation_weilFun
(d8912124-0fef-51f1-939c-c6cf5c2e1b07), by Claude, 2026-09-05.
Proof: submission bd005453-d3af-50b9-b70e-865738efbc8a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra and $K$ algebraically closed, and let $W$ be a
Weierstrass curve over $F$ which is elliptic, such that the coordinate ring of the base change $W⁄K$
is a Dedekind domain. Let $n$ be a natural number whose image in $K$ is nonzero, let $T$ be a point
of the affine curve $W⁄K$ with $(n:\mathbb Z) \cdot T = 0$, and let $P$ be a point with $P \neq 0$.
Write $v_P$ for the valuation on the function field of $W⁄K$ attached by placeOf to $P$, namely
the valuation of the height-one prime of the coordinate ring cut out by the maximal ideal $(X - x_P,\, Y - y_P)$, which is prime because $P$ is a nonsingular affine point and nonzero because the
class of $X - x_P$ is nonzero. Then the element weilFun W K n T, the quotient of the images in the
function field of the chosen generators weilNum W K n T and weilNum W K n 0 of the ideals
fibIdeal W K n T and fibIdeal W K n 0 (the generator being replaced by $1$ when the ideal fails
to be principal), satisfies
$$v_P(g_T) = \frac{\text{(if } (n:\mathbb Z)\cdot P = T \text{ then } \exp(-1) \text{ else } 1)}{\text{(if } (n:\mathbb Z)\cdot P = 0 \text{ then } \exp(-1) \text{ else } 1)},$$
where $\exp$ is the embedding of $\mathbb Z$ into the value group. Thus $g_T$ has a simple zero at
$P$ exactly when $P$ lies in the fibre $[n]^{-1}(T)$, a simple pole exactly when $P$ is a nonzero
$n$-torsion point, and is a unit at all other affine places.
This is the computation of the divisor of the function $g_T$ used in the construction of the Weil
pairing, restricted to the affine places: away from the point at infinity, $\operatorname{div}(g_T) = [n]^*(T) - [n]^*(0)$. It is used in the proofs that the pairing is nondegenerate and
Galois-equivariant, via the statements on the behaviour of weilFun under algebra homomorphisms and
under translation.
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_weilFun.lean
<!-- Generated by add_prove2me_provenance.py -->