claimstandard

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

Shows Z[2]\mathbb Z[\sqrt2] is a PID with totally positive units squares
arithmetic input for the descent images
Claim·§5 The rank-one elliptic group and its local parameters·inside propElliptic curve over F has rank one

Statement (paper)

The ring of integers of FF is OF=Z[2]\mathcal O_F=\Z[\sqrt2], and it is a principal ideal domain. Moreover, every totally positive unit of OF\mathcal O_F is a square in OF∗\mathcal O_F^*.

In plain English

The ring of integers of FF is OF=Z[2]\mathcal O_F=\Z[\sqrt2], and it is a principal ideal domain. Every totally positive unit of OF\mathcal O_F is a square in OF∗\mathcal O_F^*.

Why it's here

This is the arithmetic input for the descent computing the rank of E(F)E(F): unique factorization lets the connecting-homomorphism images be described by finitely many prime and unit classes. The fact that totally positive units are squares cuts the possible unit classes down, which is what pins down the image of α\alpha (eight classes) and the triviality of the image of α′\alpha' in the later claims.
Classified standard:
Classical facts about Q(√2): its ring of integers is Z[√2], it has class number 1, and its fundamental unit 1+√2 has norm −1, so every totally positive unit is a square (see any algebraic number theory textbook, e.g. Marcus, Number Fields).

Uses

Nothing else in the paper

Used by

claimImage of alpha has exactly eight classesclaimTrivial 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:21
Leannot aligned

Phase 2 aligns this node to a Lean declaration.