claimroutineinferred_dep

Image of alpha has exactly eight classes

Shows the image of α\alpha has exactly eight classes
fixes one factor of the descent formula
Claim·§5 The rank-one elliptic group and its local parameters·inside propElliptic curve over F has rank one

Statement (paper)

The image of α\alpha has exactly eight elements: ∣im⁡α∣=8|\operatorname{im}\alpha|=8.

In plain English

The image of the connecting homomorphism α\alpha on E(F)E(F) has exactly eight elements, so ∣im⁡α∣=8|\operatorname{im}\alpha|=8.

Why it's here

This fixes the size of one side of the 2-isogeny descent. Using that OF=Z[2]\mathcal O_F=\Z[\sqrt2] is a PID whose totally positive units are squares, the possible classes are limited to finitely many unit and prime classes, and all eight are shown to occur. Combined with the triviality of im⁡α′\operatorname{im}\alpha' in the next claim, this gives the rank-one conclusion through the isogeny index formula.
Classified routine:
Standard 2-isogeny descent computation (as in Silverman's Arithmetic of Elliptic Curves, Ch. X): the possible classes in F*/F*^2 are bounded using the PID property and unit structure of Z[√2] from the previous claim, and each candidate class is exhibited explicitly.

Uses

claimZ[√2] is a PID with square totally positive units

Used by

claimTrivial image of alpha' forces rank one

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Image of alpha has exactly eight classes" rests on claim-ell-rank-1