propositionroutine

Formal group comparison of elliptic multiples

Formal group: v(z(nP)/z(n′P))=vp(n/n′)v(z(nP)/z(n'P))=v_p(n/n') and ℓK\ell_K recovers n/n′n/n'
reads integer data off elliptic multiples locally
Proposition·ell:formal·§2.1 Elliptic indices and the local comparison

Statement (paper)

There is a fixed finite set of rational primes SES_E with the following properties. Let p∉SEp\notin S_E, let vv be any place of FF above pp, normalized by v(p)=1v(p)=1, and let n,n′∈Zn,n'\in\Z, with n′≠0n'\ne0. Assume nP,n′PnP,n'P reduce to OO at vv. Then v ⁣(z(nP)z(n′P))=vp(n/n′). v\!\left(\frac{z(nP)}{z(n'P)}\right)=v_p(n/n'). For every integer K≥1K\ge1, if in addition p>K+1p>K+1 and vp(n/n′)≥0v_p(n/n')\ge0, then ℓK(z(n′P))≠0\ell_K(z(n'P))\ne0 and v ⁣(ℓK(z(nP))ℓK(z(n′P))−nn′)≥K. v\!\left(\frac{\ell_K(z(nP))}{\ell_K(z(n'P))}-\frac n{n'}\right) \ge K. Both assertions also hold at the same place vv after replacing E,P,ℓKE,P,\ell_K by Eσ,Pσ,ℓKσE^\sigma,P^\sigma,\ell_K^\sigma and imposing the corresponding reduction-to-OO hypotheses on the conjugate points. Here and below the valuation of zero is +∞+\infty, so n=0n=0 is included.

In plain English

Outside a fixed finite set of primes SES_E, if nPnP and n′Pn'P reduce to OO at a place vv above pp, then v(z(nP)/z(n′P))=vp(n/n′)v(z(nP)/z(n'P))=v_p(n/n'). If also p>K+1p>K+1 and vp(n/n′)≥0v_p(n/n')\ge0, then ℓK(z(n′P))≠0\ell_K(z(n'P))\ne0 and ℓK(z(nP))/ℓK(z(n′P))\ell_K(z(nP))/\ell_K(z(n'P)) agrees with n/n′n/n' modulo vv-valuation at least KK; the same holds for the conjugates Eσ,Pσ,ℓKσE^\sigma,P^\sigma,\ell_K^\sigma.

Why it's here

This is the local tool that turns elliptic-curve multiples into integer arithmetic. On the formal group the parameter z(nP)z(nP) behaves like n z(P)n\,z(P) up to higher-order terms, so ratios of parameters give the pp-adic valuation of n/n′n/n' exactly, and the truncated map ℓK\ell_K recovers the rational n/n′n/n' to precision KK. The local comparison lemma and the simultaneous integer tests corollary use it to read off integer information at places of FF.
Classified routine:
A direct consequence of the standard theory of formal groups of elliptic curves, namely the formal logarithm and [n](z)=nz+⋯[n](z)=nz+\cdots on E^(pOv)\hat E(p\mathcal O_v) for good reduction primes, as in Silverman's Arithmetic of Elliptic Curves, Ch. IV and VII. The truncated-logarithm precision bound is a standard computation once p>K+1p>K+1.

Uses

Nothing else in the paper

Used by

lemLocal comparison of elliptic index with integercorSimultaneous integer tests at both places

Sources

PaperOpen
Section
§2.1 Elliptic indices and the local comparison
Page
—
Label
ell:formal
Line
sections/02-reduction.tex:109
Leannot aligned

Phase 2 aligns this node to a Lean declaration.