Valuation of the translated Weil function at finite places #
Theorem statement: WeierstrassCurve.Affine.valuation_transEquiv_weilFun
(f1fbd184-0514-54de-a553-6b93eb132cb5), by Claude, 2026-09-05.
Proof: submission e9cfbb8a-9f66-506d-9a01-dbf2314317c7, 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 an
elliptic Weierstrass curve over $F$, and assume the affine 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 $S$ be a point
of $W⁄K$, let $T$ be a point with $(n : \mathbb{Z}) \cdot T = 0$, and let $P$ be a point with $P \ne 0$. Write $v_P$ for the valuation on the function field of $W⁄K$ attached to the height-one prime
placeOf W K P hP, namely the ideal CoordinateRing.XYIdeal cut out by the affine coordinates of
$P$ (maximal, hence prime, and nonzero). Let $g_T$ be weilFun W K n T, the quotient in the
function field of the images of weilNum W K n T and weilNum W K n 0, where weilNum W K n Q
denotes a chosen generator of fibIdeal W K n Q when that ideal is principal and $1$ otherwise, and
let transEquiv W K S be the $K$-algebra automorphism of the function field given by transPull W K S, with inverse transPull W K (-S). Then, in $\mathbb{Z}_{\ge 0}$-valued notation
$\operatorname{exp}$ on WithZero (Multiplicative ℤ), $$v_P\bigl(\text{transEquiv } W\, K\, S\,(g_T)\bigr) = \frac{\bigl[\,(n:\mathbb{Z})\cdot(P+S) = T\,\bigr]}{\bigl[\,(n:\mathbb{Z})\cdot(P+S) = 0\,\bigr]},$$ where each bracket denotes
$\operatorname{exp}(-1)$ if the stated equality of points holds and $1$ otherwise.
This is the computation of the divisor of the translate $\tau_S^{*} g_T$ of the Weil function $g_T$
at the finite places of the affine coordinate ring: the order of $g_T \circ \tau_S$ at $P$ is the
order of $g_T$ at $P+S$, so that $\tau_S^{*}g_T$ has a simple zero exactly at the points $P$ with
$n(P+S) = T$ and a simple pole exactly where $n(P+S) = 0$. It is used in
[WeierstrassCurve.Affine.exists_transEquiv_weilFun_eq]
(thm.html#WeierstrassCurve.Affine.exists_transEquiv_weilFun_eq)
and thence in the identities weilPairing0_add_right and weilPairing0_self for the Weil pairing.
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_transEquiv_weilFun.lean
<!-- Generated by add_prove2me_provenance.py -->