Finiteness of the m-Selmer group when E[m] is rational

Let R be a Dedekind domain with finite residue fields and fraction field K, and let W be a Weierstrass curve over K. For each prime v of R fix a K-embedding τ v : Kˢ → K_vˢ of separable closures. A class of H¹(G_K, E[m]) is unramified outside a set S of primes when, for every v ∉ S, its restriction to K_v along τ v vanishes on the inertia subgroup of K_v (WeierstrassCurve.unramifiedOutsideTorsionCohomology).

At a prime v ∉ S where W has good reduction and which does not divide m, local Kummer classes are unramified, so every class of the m-Selmer group relative to the completions K_v is unramified outside S (WeierstrassCurve.selmerGroup_le_unramifiedOutsideTorsionCohomology).

For a rational point T ∈ E(K)[m], the Weil pairing e_m(·, T) : E[m] → μ_m carries classes unramified outside S to Kummer classes unramified outside S (WeierstrassCurve.explicitCoeff1_weilPairingCoeff_mem_unramifiedOutsideKummerCohomology), because restriction to K_v commutes with it and a coefficient map preserves vanishing on inertia. Over a number field the latter form a finite group for finite S (TauCeti.finite_unramifiedOutsideKummerCohomology). When G_K fixes every point of E(Kˢ)[m], the maps e_m(·, T) jointly detect every class (WeierstrassCurve.finite_of_forall_finite_image_explicitCoeff1_weilPairingCoeff), so the classes unramified outside a finite S are finitely many (WeierstrassCurve.finite_unramifiedOutsideTorsionCohomology), and so is the m-Selmer group (WeierstrassCurve.finite_selmerGroup_of_forall_smul_eq). This is the case E[m] ⊆ E(K) of the finiteness of Sel_m(E/K) (Silverman X.4.2), to which the general case reduces by restriction to the m-division field.

Main definitions

• WeierstrassCurve.unramifiedOutsideTorsionCohomology τ S m: the classes of H¹(G_K, E[m]) whose restriction to every K_v with v ∉ S is unramified.

Main results

• WeierstrassCurve.selmerGroup_le_unramifiedOutsideTorsionCohomology: m-Selmer classes are unramified outside the primes of bad reduction and the primes dividing m.
• WeierstrassCurve.explicitCoeff1_weilPairingCoeff_mem_unramifiedOutsideKummerCohomology: the Weil pairing with a rational m-torsion point preserves being unramified outside S.
• WeierstrassCurve.finite_unramifiedOutsideTorsionCohomology: over a number field with E[m] ⊆ E(K), finitely many classes are unramified outside a finite S.
• WeierstrassCurve.finite_selmerGroup_of_forall_smul_eq: over a number field with E[m] ⊆ E(K), the m-Selmer group relative to the completions at the finite places is finite.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.1, Proposition X.4.2 and its proof.

Weil pairings on classes unramified outside S

theorem WeierstrassCurve.explicitCoeff1_weilPairingCoeff_mem_unramifiedOutsideKummerCohomology {R : Type u_1} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {m : ℕ} [W.IsElliptic] (hm : IsUnit ↑m) (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} (hc : c ∈ W.unramifiedOutsideTorsionCohomology τ S m) : (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.weilPairingCoeff m hm T) ⋯) c ∈ TauCeti.unramifiedOutsideKummerCohomology τ S m

The Weil pairing preserves being unramified outside S. For a rational point T ∈ E(K)[m], the map H¹(G_K, E[m]) → H¹(G_K, μ_m) induced by e_m(·, T) carries classes unramified outside S to Kummer classes unramified outside S.

Finiteness over a number field

theorem WeierstrassCurve.finite_unramifiedOutsideTorsionCohomology {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) {τ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {m : ℕ} [W.IsElliptic] (hSf : S.Finite) (hm : m ≠ 0) (h : ∀ (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m), σ • P = P) : Finite ↥(W.unramifiedOutsideTorsionCohomology τ S m)

Finiteness of the classes unramified outside S when E[m] is rational. Over a number field K, if m ≠ 0, G_K fixes every point of E(Kˢ)[m] and S is finite, only finitely many classes of H¹(G_K, E[m]) are unramified outside S. Through the Weil pairing with the points of E(K)[m] they embed into finitely many copies of the finite group of Kummer classes unramified outside S.

theorem WeierstrassCurve.finite_selmerGroup_of_forall_smul_eq {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) {τ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {m : ℕ} [W.IsElliptic] (hSf : S.Finite) (hgood : ∀ v ∉ S, ∃ (x : IsIntegral (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).integer) (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))), (integralModel (↥(ValuativeRel.valuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).integer) (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))).IsElliptic) (hm : m ≠ 0) (h : ∀ (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m), σ • P = P) : Finite ↥(W.selmerGroup τ m)

Finiteness of the m-Selmer group when E[m] is rational (Silverman X.4.2, case E[m] ⊆ E(K)). Over a number field K, let W have good reduction at every prime outside a finite set S. If m ≠ 0 and G_K fixes every point of E(Kˢ)[m], the m-Selmer group of W relative to the completions of K at its finite places is finite.