Galois equivariance of the Weil pairing e₀ #
Theorem statement: WeierstrassCurve.Affine.weilPairing0_galois
(171751e8-3f74-5ac4-bd3d-1dd2af778e33), by Claude, 2026-09-05.
Proof: submission 4e2d45d6-c748-57a9-ae24-7d1a0a120f8d, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $K$ be fields with $K$ an $F$-algebra, $K$ algebraically closed, let $W$ be a
Weierstrass curve over $F$ that is elliptic, and assume 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 $\sigma$ be an
$F$-algebra automorphism of $K$, and let $S,T$ be points of the affine curve $W⁄K$ killed by $n$,
i.e. $(n:\mathbb{Z})\cdot S=0$ and $(n:\mathbb{Z})\cdot T=0$. Here $e_0(S,T)=$ weilPairing0 W K n S T is the unit of $K$ chosen so that, whenever such a unit exists, translation by $S$ on the
function field of $W⁄K$ (the automorphism transEquiv W K S, built from the translation pull-backs
along $S$ and $-S$) multiplies the function weilFun W K n T — the quotient of the images of
weilNum W K n T and weilNum W K n 0 in the function field — by the scalar $e_0(S,T)$, and is $1$
otherwise. The conclusion is that $e_0(\sigma\cdot S,\sigma\cdot T)$, viewed in $K$, equals
$\sigma\bigl(e_0(S,T)\bigr)$.
This is the Galois equivariance (Galois invariance) of the Weil pairing in its point-level form: the pairing on $n$-torsion commutes with the action of $\operatorname{Aut}(K/F)$ on points and on scalars. It is used in the construction of the Galois-equivariant Weil pairing on $n$-torsion, and thence in identifying the determinant of the mod-$n$ representation with the cyclotomic character.
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_weilPairing0_galois.lean
<!-- Generated by add_prove2me_provenance.py -->