claimroutineinferred_dep

Trivial image of alpha' forces rank one

Shows α′\alpha' has trivial image, so rank is one and mE(F)=ZPmE(F)=\mathbb ZP
concludes the rank computation
Claim·§5 The rank-one elliptic group and its local parameters·inside propElliptic curve over F has rank one

Statement (paper)

The image of the connecting homomorphism α′\alpha' on E′(F)E'(F) is trivial, im⁡α′={1}\operatorname{im}\alpha'=\{1\}. Consequently, by , rank⁡E(F)=1\operatorname{rank}E(F)=1, and for a positive integer mm divisible by the exponent of the finite torsion subgroup of E(F)E(F), the torsion-free rank-one group mE(F)mE(F) equals ZP\Z P for some nontorsion point P∈E(F)P\in E(F).

In plain English

The connecting homomorphism α′\alpha' on E′(F)E'(F) has trivial image, so the isogeny index formula gives rank⁡E(F)=1\operatorname{rank}E(F)=1. Hence for a positive integer mm divisible by the exponent of the torsion of E(F)E(F), mE(F)=ZPmE(F)=\Z P for some nontorsion point PP.

Why it's here

With ∣im⁡α∣=8|\operatorname{im}\alpha|=8 from the previous claim and ∣im⁡α′∣=1|\operatorname{im}\alpha'|=1, the descent formula 8⋅1=4⋅2rank⁡E(F)8\cdot 1=4\cdot 2^{\operatorname{rank}E(F)} gives rank one. Multiplying by such an mm kills torsion, leaving a torsion-free rank-one group, which is infinite cyclic with a generator PP; this is exactly the parent proposition's conclusion.
Classified routine:
A standard 2-isogeny descent computation (as in Silverman's or Silverman–Tate's treatment of descent via 2-isogeny) over Q(√2), using the PID and unit facts. Rank one and the cyclicity of mE(F) then follow directly from the index formula and the structure theorem for finitely generated abelian groups.

Uses

claimZ[√2] is a PID with square totally positive unitsclaimTwo-isogeny descent rank formulaclaimImage of alpha has exactly eight classes

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5 The rank-one elliptic group and its local parameters
Page
—
Label
—
Line
sections/05-elliptic.tex:77
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-1
  • info
    inferred_dep
    outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-2
  • info
    inferred_dep
    outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-3