Step 6 of the weak Mordell–Weil theorem: the image of the descent map lies in A(S,2) #
Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal
form over a field K, let R be a Dedekind domain with fraction field K, and let S be the
set of bad primes of W over R. The étale algebra W.A = K[X] ⧸ (f) splits as a product of
fields K[X] ⧸ (p), one for each monic irreducible factor p of f, and correspondingly the
square classes W.M split as a product. Define A(S,2) to be the subgroup of W.M of classes
whose component at each factor lies in the 2-Selmer group of that factor, relative to the
primes lying above S.
Step 6 is range_μ_le_selmerGroupA: the image of the descent map μ is contained in
A(S,2). Together with Step 4 (ker_μ_eq, the kernel is 2E(K)) and the finiteness of
A(S,2), this is what makes E(K)/2E(K) finite.
All the arithmetic has already been done in
TauCeti.AlgebraicGeometry.EllipticCurve.MordellWeil.BadPrimes, which proves that at a prime w
of the ring of integers of a factor not lying above a bad prime the w-adic valuation of x - θ
is even (even_valuationOfNeZero_sub_root), and that on the 2-torsion branch of μ the
component is a unit outright (valuation_projFactor_torsion_eq_one). What is left, and what this
file does, is to name the Selmer groups, record that evenness is Selmer membership
(mem_selmerGroupFactor_unit_iff, over valuationOfNeZeroMod_mk_eq_one_iff), and assemble the
componentwise statement into one about W.M along the decomposition modPowEquivPiFactors.
Main definitions #
WeierstrassCurve.Affine.selmerGroupFactor: the2-Selmer group of one field factor, relative to the primes above the bad primes.WeierstrassCurve.Affine.selmerGroupA:A(S,2), as a subgroup ofW.M. This isIsDedekindDomain.selmerGroupOfEquivat the decomposition ofW.Ainto its field factors; the product over the factors is that file'sselmerGroupPiand is not re-formed here.
Main results #
WeierstrassCurve.Affine.mem_selmerGroupFactor_unit_iff: a class of units lies in the Selmer group of a factor exactly when its valuation is even at every good prime.WeierstrassCurve.Affine.μX_component_mem_selmerGroupFactor: each component ofμX xlies in the Selmer group of its factor.WeierstrassCurve.Affine.range_μ_le_selmerGroupA: Step 6.
Roadmap #
TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (Mordell–Weil), Step 6 of the weak
Mordell–Weil theorem.
Provenance #
Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project
(github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by
TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a),
EllipticCurves/WeakMordellWeil.lean, section Selmer. The source states the square
classes as Units.modPow, a local abbreviation of its own; this repository carries a single
spelling of square classes, Mˣ ⧸ (powMonoidHom n).range, so the statements are re-spelled to it
(see TauCeti.AlgebraicGeometry.EllipticCurve.MordellWeil.XSubT for that decision). The source is
written against Lean v4.32.0; this is a forward port.
The 2-Selmer group of the field factor K[X] ⧸ (p) of W.A, relative to the primes of its
ring of integers lying above the bad primes of R.
Equations
- W.selmerGroupFactor R p = IsDedekindDomain.selmerGroupAbove R (W.ringOfIntegersFactor R p) (AdjoinRoot ↑p) (W.badPrimes R) 2
Instances For
A(S,2), as a subgroup of W.M: the classes whose image in each field factor lies in the
2-Selmer group of that factor. Step 6 asserts that im μ ≤ A(S,2).
This is IsDedekindDomain.selmerGroupOfEquiv — the Selmer group of an étale algebra transported
along a decomposition into fields — specialised to the decomposition of W.A into the factors
K[X] ⧸ (p). Stating it that way rather than re-forming the product and its comap by hand is
what makes Finite (W.selmerGroupA R) available directly from
IsDedekindDomain.finite_selmerGroupOfEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in A(S,2), componentwise: a square class lies in it exactly when each of its
components along the decomposition of W.A into field factors lies in the Selmer group of that
factor.
A(S,2) is finite, given that each factor's ring of integers has finite class group and
finitely generated unit group.
This is the finiteness that bounds the image of the descent map, and hence E(K)/2E(K).
Membership of the class of a unit in the 2-Selmer group of a field factor: its valuation is
even at every prime of the ring of integers not lying above a bad prime.
Generic case of the arithmetic input: f x ≠ 0, so the p-component of μX x is the class
of x - θ.
2-torsion case of the arithmetic input: f x = 0.
Projecting the corrected representative to the factor gives x - θ + fCofactor x, which by
valuation_projFactor_torsion_eq_one is a unit at every prime w not lying above a bad prime.
Its valuation is therefore 0, in particular even.
The heart of Step 6: for a point (x, y) of W and a field factor K[X] ⧸ (p) of W.A,
the square class of the image of the x - T map lies in the 2-Selmer group of that factor.
Step 6 of the weak Mordell–Weil theorem: the image of the descent map μ is contained in
A(S,2).