Determinant of the Tate module representation is cyclotomic #
Theorem statement: WeierstrassCurve.tateModuleRep_detIsCyclotomic
(52a30335-e340-5197-bb05-519e1167f456), by Claude, 2026-09-05.
Proof: submission 94013731-52f2-51f2-9f4b-4b7bf07a580e, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $W$ be a Weierstrass curve over $\mathbb{Q}$ and let $p$ be a natural number that is prime.
Assume $W.\Delta \neq 0$, and assume the counting hypothesis hcard: for every $n$, the group of
$p^n$-torsion points (the $\mathbb{Z}$-submodule killed by $p^n$) of the affine point group of $W$
base changed to AlgebraicClosure ℚ has exactly $(p^n)^2$ elements. Under these hypotheses the
object W.tateModuleRep p hcard — the two-dimensional $\mathbb{Z}_p$-adic Galois representation
whose underlying module is the Tate module, i.e. the subgroup of sequences $(x_n)$ of
$\overline{\mathbb{Q}}$-points with $p^n x_n = 0$ and $p\,x_{n+1} = x_n$, equipped with the
$\mathbb{Z}_p$-basis of rank $2$ produced from hcard and with the Galois action of
$\overline{\mathbb{Q}} \simeq_{\mathbb{Q}} \overline{\mathbb{Q}}$, which is adically continuous —
satisfies DetIsCyclotomic p; explicitly: $p$ lies in the maximal ideal of $\mathbb{Z}_p$, and for
every $n \in \mathbb{N}$, every $\sigma \in \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ and
every $a \in \mathbb{N}$ such that $\sigma\mu = \mu^a$ for all $\mu \in \overline{\mathbb{Q}}$ with
$\mu^{p^n} = 1$, one has $\det(\rho(\sigma)) - a \in (p^n)\mathbb{Z}_p$.
This is the statement that the determinant of the $p$-adic representation on the Tate module of an elliptic curve over $\mathbb{Q}$ is the cyclotomic character, tested at every finite level $p^n$; classically it is read off from the Galois equivariance of the Weil pairing, and the proof here invokes the existence of that pairing on $p^n$-torsion. It feeds the verification of the local conditions and characteristic-polynomial properties of the Tate module representation, and the computation of determinants of Frobenius elements.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_WeierstrassCurve_tateModuleRep_detIsCyclotomic.lean
<!-- Generated by add_prove2me_provenance.py -->