claimroutine

Two-torsion Kummer classes are independent

Shows two-torsion Kummer classes τ1,τ2\tau_1,\tau_2 are independent
identifies two-torsion inside the Selmer group
Claim·§3.3 A criterion for one twist·inside lemTwo-descent criterion for twist E_l

Statement (paper)

In the Kummer coordinates (x+3l,x−l)(x+3l,x-l), the points (l,0)(l,0) and (−3l,0)(-3l,0) of ElE_l have classes τ1=(l,1)\tau_1=(l,1) and τ2=(3,−l)\tau_2=(3,-l) respectively, and these two classes are independent globally (linearly independent over F2\F_2 in the global Kummer group).

In plain English

In the Kummer coordinates (x+3l,x−l)(x+3l,x-l), the two-torsion points (l,0)(l,0) and (−3l,0)(-3l,0) of ElE_l map to τ1=(l,1)\tau_1=(l,1) and τ2=(3,−l)\tau_2=(3,-l). These two classes are linearly independent over F2\F_2 in the global Kummer group.

Why it's here

This identifies the rational two-torsion subgroup inside the Selmer group as a two-dimensional subspace. The parent lemma needs this to say that the Selmer class (β,1)(\beta,1) lies outside the rational two-torsion classes, and the later local-image claims use it. Independence follows because l>1l>1 is squarefree, so ll and −l-l are not squares in Q\Q, and 33 is not a square; hence τ1\tau_1, τ2\tau_2 and τ1τ2\tau_1\tau_2 are all nontrivial.
Classified routine:
Direct computation with the standard 2-descent Kummer map for an elliptic curve with full rational 2-torsion (e.g. Silverman, The Arithmetic of Elliptic Curves, X.1), plus the observation that l, -l, 3 and their products are non-squares in Q.

Uses

Nothing else in the paper

Used by

claimLocal Kummer images at odd primes and 3claimNormalized Selmer pairs with positive coordinates

Sources

PaperOpen
Section
§3.3 A criterion for one twist
Page
—
Label
—
Line
sections/03-parity.tex:318
Leannot aligned

Phase 2 aligns this node to a Lean declaration.