Multiplicativity of e₀ in the first variable #
Theorem statement: WeierstrassCurve.Affine.weilPairing0_add_left
(d88a7ffc-2012-5fc9-875c-d348fbe7cc18), by Claude, 2026-09-05.
Proof: submission 0dd5d3ef-3ee2-5e32-a678-ceed9023d8c5, 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$ which is elliptic, and assume the coordinate ring of the base change $W\!\restriction_K$ is a Dedekind domain. Let $n$ be a natural number whose image in $K$ is nonzero, and let $S$, $S'$, $T$ be points of the group $(W⁄K).\mathrm{Point}$ with $n\cdot S = n\cdot S' = n\cdot T = 0$ (scalar multiplication by $(n : \mathbb{Z})$). Here $\mathrm{weilPairing0}\,W\,K\,n\,S\,T \in K^\times$ is defined to be a chosen unit $c$ such that the automorphism $\mathrm{transEquiv}\,W\,K\,S$ of the function field of $W\!\restriction_K$ (the algebra automorphism obtained from pullback along translation by $S$, with inverse the pullback along translation by $-S$) sends $\mathrm{weilFun}\,W\,K\,n\,T$ — the ratio of the images in the function field of $\mathrm{weilNum}\,W\,K\,n\,T$ and of $\mathrm{weilNum}\,W\,K\,n\,0$ — to $c \cdot \mathrm{weilFun}\,W\,K\,n\,T$, and $1$ if no such unit exists. The conclusion is the identity $\mathrm{weilPairing0}\,W\,K\,n\,(S+S')\,T = \mathrm{weilPairing0}\,W\,K\,n\,S\,T \cdot \mathrm{weilPairing0}\,W\,K\,n\,S'\,T$ in $K^\times$.
This is bilinearity of the Weil pairing in its first argument, at the level of the scalar attached to the translation-invariance of the function $g_T$. It feeds the group-theoretic properties of the $n$-torsion pairing used later in the analysis of level structures on modular curves, in particular the determinant computations for the action on full-level and $\Gamma_0$-type structures.
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_add_left.lean
<!-- Generated by add_prove2me_provenance.py -->