The formal point, the filtration, and the structure of E(K_v) #
Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.
Building on the valuation estimates, this file constructs the point (t/w(t), -1/w(t)) of
E(K_v) attached to an šŖ-point of the formal group (formalPoint), proves the parametrization
is additive, and defines the filtration E_{n+1}(K_v) of points whose x-coordinate has a pole
of order at least 2(n+1). It then proves torsion-freeness of the kernel of reduction Eā(K_v)
under the standard ramification condition, that every filtration step has finite index, and the
structure theorem: E(K_v) has a finite-index subgroup isomorphic to (šŖ_v, +).
theorem
WeierstrassCurve.Affine.formalPoint_nonsingular
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
{t : ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
(ht : t ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(ht0 : t ā 0)
:
W.Nonsingular (āt / ā(Wā.wEval t)) (-1 / ā(Wā.wEval t))
The parametrized point of the kernel of reduction attached to a parameter t ā šŖ,
t ā 0, is nonsingular.
noncomputable def
WeierstrassCurve.Affine.formalPoint
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
(z : Wā.formalGroupLaw.Points)
:
W.Point
The point of the kernel of reduction attached to an šŖ-point of the formal group of
the integral model Wā: the parameter t gives the affine point (t/w(t), -1/w(t)),
and t = 0 gives the point at infinity.
Equations
Instances For
@[simp]
theorem
WeierstrassCurve.Affine.formalPoint_of_param_eq_zero
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
{z : Wā.formalGroupLaw.Points}
(h0 : ā(z ()) = 0)
:
theorem
WeierstrassCurve.Affine.formalPoint_of_param_ne_zero
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
{z : Wā.formalGroupLaw.Points}
(h0 : ā(z ()) ā 0)
:
theorem
WeierstrassCurve.Affine.formalPoint_injective
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
:
The parametrization of the kernel of reduction is injective.
theorem
WeierstrassCurve.Affine.exists_formalPoint_eq_some
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
{x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v}
(h : W.Nonsingular x y)
(hx : WithZero.exp 2 ā¤ Valued.v x)
:
ā (z : Wā.formalGroupLaw.Points), formalPoint hW z = Point.some x y h
Every affine point with a pole of order at least 2 at x comes from a parameter
in šŖ.
theorem
WeierstrassCurve.Affine.formalPoint_eq_zero_iff
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
{z : Wā.formalGroupLaw.Points}
:
theorem
WeierstrassCurve.Affine.formalPoint_negPoint
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
(z : Wā.formalGroupLaw.Points)
:
The parametrization intertwines the formal inverse with negation of points.
theorem
WeierstrassCurve.Affine.formalPoint_add
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
(z z' : Wā.formalGroupLaw.Points)
:
The parametrization of the kernel of reduction is additive.
def
WeierstrassCurve.Affine.filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
(n : ā)
:
For an elliptic curve W over K_v with an integral model Wā and n : ā, the
subgroup E_{n+1}(K_v) of points (x, y) with exp (2 * (n + 1)) ā¤ v(x) (a pole of order
at least 2(n + 1) at x, together with 0); this is the kernel of reduction modulo
šŖ^(n+1), isomorphic to the group Ć(šŖ^(n+1)) of points of the formal group of Wā
(Silverman, VII.2.2). Closure under addition comes from the formal group: both summands
are parametrized by šŖ^(n+1)-parameters, and the addition series preserves that level.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
WeierstrassCurve.Affine.zero_mem_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{n : ā}
:
@[simp]
theorem
WeierstrassCurve.Affine.some_mem_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{n : ā}
{x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v}
{h : W.Nonsingular x y}
:
theorem
WeierstrassCurve.Affine.mem_pow_iff_formalPoint_mem_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
(z : Wā.formalGroupLaw.Points)
(n : ā)
:
ā(z ()) ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (n + 1) ā formalPoint hW z ā filtration hW n
The filtration correspondence: the parameter lies in šŖ^(n+1) exactly when the
associated point lies in the filtration step E_{n+1}(K_v).
theorem
WeierstrassCurve.Affine.formalPoint_surjective
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{P : W.Point}
(hP : P ā filtration hW 0)
:
ā (z : Wā.formalGroupLaw.Points), formalPoint hW z = P
Every point of the kernel of reduction comes from a parameter in šŖ: the
parametrization by the šŖ-points of the formal group is surjective onto
filtration hW 0.
theorem
WeierstrassCurve.Affine.exists_points_equiv_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
:
ā (Īø : Wā.formalGroupLaw.Points ā+ ā„(filtration hW 0)),
ā (z : Wā.formalGroupLaw.Points) (n : ā),
ā(z ()) ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (n + 1) ā ā(Īø z) ā filtration hW n
The šŖ-points of the formal group law of an integral model Wā of W are the kernel
of reduction Eā(K_v) = filtration hW 0, via z ā¦ (x, y) with x = z/w(z),
y = -1/w(z); the equivalence matches the filtration by valuation on both sides
(Silverman, VII.2.2).
theorem
WeierstrassCurve.Affine.filtration_anti
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{m n : ā}
(hmn : m ā¤ n)
:
The filtration is decreasing.
theorem
WeierstrassCurve.Affine.eq_zero_of_isOfFinAddOrder_of_mem_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{p : ā}
(hp : Nat.Prime p)
(hpmem : āp ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(hpram : āp ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (p - 1))
{P : W.Point}
(hP : P ā filtration hW 0)
(hord : IsOfFinAddOrder P)
:
The kernel of reduction is torsion-free under the standard ramification condition
(Silverman VII.3.1(b)/VII.3.4): if the residue characteristic p satisfies
(p : šŖ_v) ā šŖ^(p-1) ā that is, e < p ā 1 for the absolute ramification index e ā
then Eā(K_v) contains no nonzero point of finite order. Consequently the torsion of
E(K_v) (and of any subgroup, such as the image of E(K)) injects into the reduction
E(K_v)/Eā(K_v).
theorem
WeierstrassCurve.Affine.isOfFinAddOrder.eq_of_sub_mem_filtration
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
{hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W}
{p : ā}
(hp : Nat.Prime p)
(hpmem : āp ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(hpram : āp ā IsLocalRing.maximalIdeal ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (p - 1))
{P Q : W.Point}
(hP : IsOfFinAddOrder P)
(hQ : IsOfFinAddOrder Q)
(h : P - Q ā filtration hW 0)
:
Torsion points of E(K_v) with the same image modulo the kernel of reduction agree:
the reduction map is injective on torsion under the ramification condition.
theorem
WeierstrassCurve.Affine.filtration_zero_finiteIndex
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
[Finite (R ā§ø v.asIdeal)]
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
:
(filtration hW 0).FiniteIndex
The kernel of reduction has finite index in E(K_v): the complement consists of
integral points, which a compactness argument covers by finitely many congruence
neighbourhoods.
theorem
WeierstrassCurve.Affine.filtration_finiteIndex
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
[Finite (R ā§ø v.asIdeal)]
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
(n : ā)
:
(filtration hW n).FiniteIndex
Each step of the valuation filtration on the points of an elliptic curve over K_v has
finite index, by induction: each step has finite index in the previous one
(relIndex_filtration_succ_ne_zero), and the 0-th step has finite index in E(K_v).
theorem
WeierstrassCurve.Affine.exists_filtration_equiv
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
{v : IsDedekindDomain.HeightOneSpectrum R}
{W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
{Wā : WeierstrassCurve ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}
[WeierstrassCurve.IsElliptic W]
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
[Finite (R ā§ø v.asIdeal)]
(hW :
Wā.map
(algebraMap (ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
(IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W)
:
ā (n : ā), Nonempty (ā„(filtration hW n) ā+ ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
Some step of the valuation filtration on the points of an elliptic curve over K_v is
isomorphic to the additive group of šŖ_v: for šŖ^k past the ramification of the residue
characteristic, the scaled formal logarithm identifies Ć(šŖ^k) with (šŖ^k, +) ā
(šŖ_v, +)
(Silverman, IV.6.4).
theorem
WeierstrassCurve.Affine.exists_finiteIndex_addSubgroup_equiv_adicCompletionIntegers
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{K : Type u_2}
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : IsDedekindDomain.HeightOneSpectrum R)
[DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)]
[CharZero K]
[Finite (R ā§ø v.asIdeal)]
(W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))
[WeierstrassCurve.IsElliptic W]
:
ā (U : AddSubgroup W.Point),
U.FiniteIndex ā§ Nonempty (ā„U ā+ ā„(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))
The group of points of an elliptic curve over the completion K_v (a characteristic-0
local field with finite residue field) has a subgroup of finite index that is isomorphic to
the additive group of the valuation ring šŖ_v.
This is the structure theorem coming from the formal group of the curve: pass to an integral model and take a suitable step of the valuation filtration.