The m-Selmer group and the Shafarevich–Tate group of an elliptic curve

Let W be an elliptic curve over a field K, with Galois cohomology taken in the discrete G_K-modules E(Kˢ) and E(Kˢ)[m]. Fix a family (L i) of field extensions of K, each with a K-embedding τ i : Kˢ →ₐ[K] (L i)ˢ of separable closures. Restriction along τ i (WeierstrassCurve.pointRes) is the localisation map to L i, and Silverman's definitions read (X.4):

Sha = ker (H¹(G_K, E(Kˢ)) → ∏ᵢ H¹(G_{L i}, E((L i)ˢ))),
Sel_m = ker (H¹(G_K, E(Kˢ)[m]) → ∏ᵢ H¹(G_{L i}, E((L i)ˢ))).

For a number field K and the family of its completions at all places, these are the Shafarevich–Tate group Sha(E/K) and the m-Selmer group Sel_m(E/K). Here they are defined for an arbitrary family, as WeierstrassCurve.shafarevichTateGroup and WeierstrassCurve.selmerGroup, the Selmer groups (TauCeti.ContCohomology.SelmerStructure.selmerGroup) of two Selmer structures localising along the restriction maps τ i: on E(Kˢ) with the zero local conditions, and on E(Kˢ)[m] with the local conditions ker (H¹(G_{L i}, E[m]) → H¹(G_{L i}, E)). The homomorphism G_{L i} → G_K used for pullback requires a choice of embedding. The induced cohomology maps and the resulting subgroups are independent of this choice, as proved in TauCeti/AlgebraicGeometry/EllipticCurve/GaloisCohomology/EmbeddingIndependence.lean.

These kernel-based definitions need no hypothesis on m or on W. When W is elliptic and m is invertible in K, the Selmer group is cut out by local Kummer conditions: a class lies in Sel_m exactly when its restriction to each L i lies in the image of the local Kummer map E(L i) → H¹(G_{L i}, E[m]) (WeierstrassCurve.mem_selmerGroup_iff_forall_torsionRes_mem_range_kummerMap). This is the form in which local conditions are checked in practice, and it follows from the compatibility of restriction with the Kummer maps and from the local m-descent sequence.

Under the same hypotheses, the main result is the m-descent sequence (Silverman X.4.2)

0 ⟶ E(K) ⧸ m E(K) ⟶ Sel_m ⟶ Sha[m] ⟶ 0,

obtained by restricting the global sequence 0 → E(K) ⧸ m E(K) → H¹(G_K, E[m]) → H¹(G_K, E)[m] → 0 of TauCeti/AlgebraicGeometry/EllipticCurve/GaloisCohomology/Descent.lean to the Selmer group.

Main definitions

• WeierstrassCurve.shaSelmerStructure: the Selmer structure on E(Kˢ) with zero local conditions.
• WeierstrassCurve.selmerStructure: the Selmer structure on E(Kˢ)[m] whose local condition at L i is the kernel of H¹(G_{L i}, E[m]) → H¹(G_{L i}, E); for W elliptic and m invertible in K, this is the image of the local Kummer map.
• WeierstrassCurve.shafarevichTateGroup: the classes in H¹(G_K, E(Kˢ)) that restrict to zero over every L i.
• WeierstrassCurve.selmerGroup: the classes in H¹(G_K, E(Kˢ)[m]) whose image in H¹(G_K, E(Kˢ)) lies in the Shafarevich–Tate group.
• WeierstrassCurve.kummerSelmerMap: the Kummer map E(K) ⧸ m E(K) → Sel_m.
• WeierstrassCurve.selmerShaMap: the map Sel_m → Sha[m].

Main results

• WeierstrassCurve.mem_selmerGroup_iff_forall_torsionRes_mem_range_kummerMap: the Selmer group is cut out by the images of the local Kummer maps.
• WeierstrassCurve.kummerMap_mem_selmerGroup: Kummer classes of points of E(K) are Selmer.
• WeierstrassCurve.kummerSelmerMap_injective, WeierstrassCurve.exact_kummerSelmerMap_selmerShaMap and WeierstrassCurve.selmerShaMap_surjective: the m-descent sequence 0 → E(K) ⧸ m E(K) → Sel_m → Sha[m] → 0 is exact.

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.4.

The Shafarevich–Tate group

noncomputable def WeierstrassCurve.shaSelmerStructure {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) : TauCeti.ContCohomology.SelmerStructure (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff (fun (i : ι) => TauCeti.AbsoluteGaloisGroup (L i)) fun (i : ι) => (W.baseChange (L i)).PointCoeff

The Selmer structure of the Shafarevich–Tate group: on E(Kˢ), localised along the restriction maps τ i, with the zero local condition at every L i.

@[simp]

theorem WeierstrassCurve.shaSelmerStructure_localization {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (i : ι) : (W.shaSelmerStructure τ).localization i = W.pointRes (τ i)

The localisation maps of shaSelmerStructure τ are the restriction maps pointRes (τ i).

@[simp]

theorem WeierstrassCurve.shaSelmerStructure_localCondition {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (i : ι) : (W.shaSelmerStructure τ).localCondition i = ⊥

noncomputable def WeierstrassCurve.shafarevichTateGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) : AddSubgroup (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff)

The Shafarevich–Tate group of W relative to the family of extensions L i with embeddings τ i: the Selmer group of shaSelmerStructure τ, that is, the classes in H¹(G_K, E(Kˢ)) whose restriction to every L i vanishes. For a number field and the family of its completions at all places this is Sha(E/K) (Silverman X.4).

@[simp]

theorem WeierstrassCurve.mem_shafarevichTateGroup_iff {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff} : c ∈ W.shafarevichTateGroup τ ↔ ∀ (i : ι), (W.pointRes (τ i)) c = 0

theorem WeierstrassCurve.shafarevichTateGroup_le_comp {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {κ : Type u_4} (f : κ → ι) : W.shafarevichTateGroup τ ≤ W.shafarevichTateGroup fun (j : κ) => τ (f j)

Imposing local triviality along a subfamily τ ∘ f of the localisations gives a larger Shafarevich–Tate group.

The Selmer group

noncomputable def WeierstrassCurve.selmerStructure {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) : TauCeti.ContCohomology.SelmerStructure (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (fun (i : ι) => TauCeti.AbsoluteGaloisGroup (L i)) fun (i : ι) => (W.baseChange (L i)).TorsionCoeff m

The Selmer structure of the m-Selmer group: on E(Kˢ)[m], localised along the restriction maps τ i, with local condition at L i the kernel of H¹(G_{L i}, E[m]) → H¹(G_{L i}, E). When W is elliptic and m is invertible in K, this kernel is the image of the local Kummer map E(L i) → H¹(G_{L i}, E[m]) (WeierstrassCurve.mem_selmerGroup_iff_forall_torsionRes_mem_range_kummerMap).

@[simp]

theorem WeierstrassCurve.selmerStructure_localization {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) (i : ι) : (W.selmerStructure τ m).localization i = W.torsionRes (τ i) m

The localisation maps of selmerStructure τ m are the restriction maps torsionRes (τ i) m.

@[simp]

theorem WeierstrassCurve.selmerStructure_localCondition {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) (i : ι) : (W.selmerStructure τ m).localCondition i = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup (L i)) ((W.baseChange (L i)).TorsionCoeff m) ((W.baseChange (L i)).torsionCoeffIncl m) ⋯).ker

noncomputable def WeierstrassCurve.selmerGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) : AddSubgroup (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m))

The m-Selmer group of W relative to the family of extensions L i with embeddings τ i: the Selmer group of selmerStructure τ m, that is, the classes in H¹(G_K, E(Kˢ)[m]) whose image in H¹(G_K, E(Kˢ)) lies in the Shafarevich–Tate group (mem_selmerGroup_iff). For a number field and the family of its completions at all places this is Sel_m(E/K) (Silverman X.4).

@[simp]

theorem WeierstrassCurve.mem_selmerGroup_iff {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : c ∈ W.selmerGroup τ m ↔ (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯) c ∈ W.shafarevichTateGroup τ

theorem WeierstrassCurve.selmerGroup_le_comp {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) {κ : Type u_4} (f : κ → ι) : W.selmerGroup τ m ≤ W.selmerGroup (fun (j : κ) => τ (f j)) m

Imposing the local conditions along a subfamily τ ∘ f of the localisations gives a larger m-Selmer group.

theorem WeierstrassCurve.mem_selmerGroup_iff_forall_torsionRes_mem_range_kummerMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [W.IsElliptic] [(i : ι) → DecidableEq (L i)] (hm : IsUnit ↑m) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : c ∈ W.selmerGroup τ m ↔ ∀ (i : ι), (W.torsionRes (τ i) m) c ∈ ((W.baseChange (L i)).kummerMap m ⋯).range

The Selmer group is cut out by the local Kummer images: a class in H¹(G_K, E(Kˢ)[m]) is Selmer exactly when its restriction to every L i comes from a point of E(L i) under the local Kummer map.

The m-descent sequence

theorem WeierstrassCurve.kummerMap_mem_selmerGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [DecidableEq K] [W.IsElliptic] (hm : IsUnit ↑m) (P : W.toAffine.Point) : (W.kummerMap m hm) P ∈ W.selmerGroup τ m

Kummer classes are Selmer: the Kummer class of a point of E(K) lies in the Selmer group, since it already vanishes in H¹(G_K, E(Kˢ)).

noncomputable def WeierstrassCurve.kummerSelmerMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [DecidableEq K] [W.IsElliptic] (hm : IsUnit ↑m) : W.toAffine.Point ⧸ (nsmulAddMonoidHom m).range →+ ↥(W.selmerGroup τ m)

The Kummer map E(K) ⧸ m E(K) → Sel_m, the first map of the m-descent sequence.

@[simp]

theorem WeierstrassCurve.coe_kummerSelmerMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [DecidableEq K] [W.IsElliptic] (hm : IsUnit ↑m) (x : W.toAffine.Point ⧸ (nsmulAddMonoidHom m).range) : ↑((W.kummerSelmerMap τ hm) x) = (W.kummerClassMap m hm) x

theorem WeierstrassCurve.kummerSelmerMap_injective {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [DecidableEq K] [W.IsElliptic] (hm : IsUnit ↑m) : Function.Injective ⇑(W.kummerSelmerMap τ hm)

E(K) ⧸ m E(K) injects into the Selmer group.

noncomputable def WeierstrassCurve.selmerShaMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) : ↥(W.selmerGroup τ m) →+ ↥(AddSubgroup.torsionBy ↥(W.shafarevichTateGroup τ) ↑m)

The map Sel_m → Sha[m], the second map of the m-descent sequence: the map induced by the inclusion E(Kˢ)[m] → E(Kˢ), restricted to the Selmer group.

@[simp]

theorem WeierstrassCurve.coe_selmerShaMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) (m : ℕ) (c : ↥(W.selmerGroup τ m)) : ↑↑((W.selmerShaMap τ m) c) = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯) ↑c

theorem WeierstrassCurve.exact_kummerSelmerMap_selmerShaMap {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [DecidableEq K] [W.IsElliptic] (hm : IsUnit ↑m) : Function.Exact ⇑(W.kummerSelmerMap τ hm) ⇑(W.selmerShaMap τ m)

The m-descent sequence is exact at Sel_m: the kernel of Sel_m → Sha[m] is the image of E(K) ⧸ m E(K) under the Kummer map.

theorem WeierstrassCurve.selmerShaMap_surjective {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_2} {L : ι → Type u_3} [(i : ι) → Field (L i)] [(i : ι) → Algebra K (L i)] (τ : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (L i)) {m : ℕ} [W.IsElliptic] (hm : IsUnit ↑m) : Function.Surjective ⇑(W.selmerShaMap τ m)

Sel_m → Sha[m] is surjective, the right end of the m-descent sequence: a class of Sha killed by m lifts to H¹(G_K, E(Kˢ)[m]) by the global descent sequence, and every lift is Selmer.