The semilocal comparison of 2-descent at the good finite places

Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal form over a number field F, with étale algebra W.A = F[X] ⧸ (f) and square classes W.M. Two subgroups of W.M cut out by valuation conditions are in play:

• W.selmerGroupA (𝓞 F) — the S-unramifiedness condition A(S,2), a global condition at the primes of the rings of integers of the field factors of W.A not lying above a bad prime;
• (W⁄F_v).toAffine.selmerGroupA 𝒪_v — the same condition for the curve base-changed to the completion at a finite place v.

This file compares the two at the good finite places, in both directions: an S-unramified class localizes to an unramified class at each good place, and conversely a class that localizes to an unramified class at every good place is S-unramified. That is what makes the local conditions at the good finite places redundant — they are already implied by A(S,2) — so membership in the 2-Selmer group reduces to the finitely many conditions at the bad and infinite places.

Main results

• WeierstrassCurve.Affine.localRes_mem_selmerGroupA (global to local): an S-unramified square class localizes to an unramified class at every good finite place.
• WeierstrassCurve.Affine.mem_selmerGroupA_of_forall_localRes (local to global): a square class that localizes to an unramified class at every good finite place is S-unramified.

Provenance

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, Apache 2.0, by Michael Stoll) at commit 66889eada51a: EllipticCurves/SelmerGroup.lean, section Semilocal, together with AdjoinRoot.map_comp_algebraMap from EllipticCurves/Mathlib/Basic.lean. The source states square classes as its own Units.modPow; they are re-spelled here to this repository's single spelling Mˣ ⧸ (powMonoidHom n).range, and HeightOneSpectrum.below is Mathlib's HeightOneSpectrum.under.

theorem WeierstrassCurve.Affine.localRes_mem_selmerGroupA {F : Type u_1} [Field F] [NumberField F] (W : Affine F) [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers F)} (hv : v ∉ W.badPrimes (NumberField.RingOfIntegers F)) {m : M} (hm : m ∈ W.selmerGroupA (NumberField.RingOfIntegers F)) : (W.localRes (IsDedekindDomain.HeightOneSpectrum.adicCompletion F v)) m ∈ (toAffine (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F v))).selmerGroupA ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)

Semilocal comparison, global to local: an S-unramified square class localizes to an unramified class at every good finite place.

theorem WeierstrassCurve.Affine.mem_selmerGroupA_of_forall_localRes {F : Type u_1} [Field F] [NumberField F] (W : Affine F) [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] {m : M} (hm : ∀ v ∉ W.badPrimes (NumberField.RingOfIntegers F), (W.localRes (IsDedekindDomain.HeightOneSpectrum.adicCompletion F v)) m ∈ (toAffine (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F v))).selmerGroupA ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F v)) : m ∈ W.selmerGroupA (NumberField.RingOfIntegers F)

Semilocal comparison, local to global: a square class that localizes to an unramified class at every good finite place is S-unramified.