Restriction in towers, and restriction of Selmer groups

Let W be a Weierstrass curve over a field K and K → L → M a tower of field extensions. Restriction of the Galois cohomology of W is transitive: restricting from K to L and then from L to M is restricting from K to M,

H¹(G_K, E(Kˢ)) → H¹(G_L, E(Lˢ)) → H¹(G_M, E(Mˢ))   =   H¹(G_K, E(Kˢ)) → H¹(G_M, E(Mˢ)),

up to the identification of the coefficients of (W⁄L)⁄M with those of W⁄M (WeierstrassCurve.pointRes_pointRes, WeierstrassCurve.torsionRes_torsionRes). Since restriction does not depend on the embeddings of separable closures, any embedding Kˢ → Mˢ may be used on the right.

The main consequence is that restriction to an extension L/K carries the Shafarevich–Tate and Selmer groups of W into those of W⁄L (WeierstrassCurve.pointRes_mem_shafarevichTateGroup, WeierstrassCurve.torsionRes_mem_selmerGroup). Here the local fields L' j defining the groups over L must each lie over one of the local fields K' (σ j) defining the groups over K, as the completion L_w of a number field lies over the completion K_v at the place v below w: a class vanishing over K_v vanishes over L_w, and the two towers K → L → L_w and K → K_v → L_w give the same restriction to L_w. For L = K(E[m]) this reduces the finiteness of Sel_m(E/K) to the finiteness of Sel_m(E/L) together with the finiteness of the kernel of restriction to L (Silverman, the proof of X.4.2).

Main results

• WeierstrassCurve.pointRes_pointRes, WeierstrassCurve.torsionRes_torsionRes: restriction is transitive in towers.
• WeierstrassCurve.pointRes_pointRes_eq_zero_iff, WeierstrassCurve.torsionRes_torsionRes_eq_zero_iff: a class restricts to zero along a tower exactly when it restricts to zero directly.
• WeierstrassCurve.pointRes_mem_shafarevichTateGroup: restriction maps Sha(E/K) into Sha(E/L).
• WeierstrassCurve.torsionRes_mem_selmerGroup: restriction maps Sel_m(E/K) into Sel_m(E/L).
• WeierstrassCurve.finite_selmerGroup_of_finite_ker_torsionRes: Sel_m(E/K) is finite if Sel_m(E/L) is and restriction to L has finite kernel.

Implementation notes

The identification of (W⁄L)⁄M with W⁄M is Mathlib's WeierstrassCurve.map_baseChange at IsScalarTower.toAlgHom K L M, restated by show in terms of base change, as in WeierstrassCurve.pointCoeffBaseChange_pointCoeffBaseChange.

References

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

Restriction in a tower

theorem WeierstrassCurve.pointRes_pointRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {M : Type u_3} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (τ' : SeparableClosure L →ₐ[L] SeparableClosure M) (τ'' : SeparableClosure K →ₐ[K] SeparableClosure M) (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff) : ((W.baseChange L).pointRes τ') ((W.pointRes τ) c) = (TauCeti.ContCohomology.explicitCoeff1Equiv (TauCeti.AbsoluteGaloisGroup M) (W.baseChange M).PointCoeff (AddEquiv.cast ⋯) ⋯ ⋯ ⋯) ((W.pointRes τ'') c)

Restriction on H¹(G_K, E(Kˢ)) is transitive in a tower K → L → M: restricting to L along τ and then to M along τ' is restricting to M along any embedding τ'' : Kˢ → Mˢ, followed by the identification of (W⁄L)⁄M with W⁄M.

theorem WeierstrassCurve.torsionRes_torsionRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {M : Type u_3} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (τ' : SeparableClosure L →ₐ[L] SeparableClosure M) (τ'' : SeparableClosure K →ₐ[K] SeparableClosure M) (m : ℕ) (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : ((W.baseChange L).torsionRes τ' m) ((W.torsionRes τ m) c) = (TauCeti.ContCohomology.explicitCoeff1Equiv (TauCeti.AbsoluteGaloisGroup M) ((W.baseChange M).TorsionCoeff m) (AddEquiv.cast ⋯) ⋯ ⋯ ⋯) ((W.torsionRes τ'' m) c)

Restriction on H¹(G_K, E(Kˢ)[m]) is transitive in a tower K → L → M, as in WeierstrassCurve.pointRes_pointRes.

theorem WeierstrassCurve.pointRes_pointRes_eq_zero_iff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {M : Type u_3} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (τ' : SeparableClosure L →ₐ[L] SeparableClosure M) (τ'' : SeparableClosure K →ₐ[K] SeparableClosure M) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff} : ((W.baseChange L).pointRes τ') ((W.pointRes τ) c) = 0 ↔ (W.pointRes τ'') c = 0

A class of H¹(G_K, E(Kˢ)) restricts to zero along the tower K → L → M exactly when it restricts to zero along any embedding Kˢ → Mˢ.

theorem WeierstrassCurve.torsionRes_torsionRes_eq_zero_iff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {M : Type u_3} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (τ' : SeparableClosure L →ₐ[L] SeparableClosure M) (τ'' : SeparableClosure K →ₐ[K] SeparableClosure M) {m : ℕ} {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : ((W.baseChange L).torsionRes τ' m) ((W.torsionRes τ m) c) = 0 ↔ (W.torsionRes τ'' m) c = 0

A class of H¹(G_K, E(Kˢ)[m]) restricts to zero along the tower K → L → M exactly when it restricts to zero along any embedding Kˢ → Mˢ.

Restriction of the Shafarevich–Tate and Selmer groups

theorem WeierstrassCurve.pointRes_mem_shafarevichTateGroup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {ι : Type u_3} {K' : ι → Type u_4} [(i : ι) → Field (K' i)] [(i : ι) → Algebra K (K' i)] (τK : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (K' i)) {J : Type u_5} {L' : J → Type u_6} [(j : J) → Field (L' j)] [(j : J) → Algebra L (L' j)] (τL : (j : J) → SeparableClosure L →ₐ[L] SeparableClosure (L' j)) (σ : J → ι) [(j : J) → Algebra K (L' j)] [∀ (j : J), IsScalarTower K L (L' j)] [(j : J) → Algebra (K' (σ j)) (L' j)] [∀ (j : J), IsScalarTower K (K' (σ j)) (L' j)] {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff} (hc : c ∈ W.shafarevichTateGroup τK) : (W.pointRes τ) c ∈ (W.baseChange L).shafarevichTateGroup τL

Restriction maps Sha(E/K) into Sha(E/L). If each field L' j defining the Shafarevich–Tate group of W⁄L is an extension of the field K' (σ j) defining that of W, compatibly with K → L → L' j, then restriction to L carries the Shafarevich–Tate group of W into that of W⁄L: a class vanishing over K' (σ j) vanishes over L' j.

theorem WeierstrassCurve.torsionRes_mem_selmerGroup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {ι : Type u_3} {K' : ι → Type u_4} [(i : ι) → Field (K' i)] [(i : ι) → Algebra K (K' i)] (τK : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (K' i)) {J : Type u_5} {L' : J → Type u_6} [(j : J) → Field (L' j)] [(j : J) → Algebra L (L' j)] (τL : (j : J) → SeparableClosure L →ₐ[L] SeparableClosure (L' j)) (σ : J → ι) [(j : J) → Algebra K (L' j)] [∀ (j : J), IsScalarTower K L (L' j)] [(j : J) → Algebra (K' (σ j)) (L' j)] [∀ (j : J), IsScalarTower K (K' (σ j)) (L' j)] {m : ℕ} {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} (hc : c ∈ W.selmerGroup τK m) : (W.torsionRes τ m) c ∈ (W.baseChange L).selmerGroup τL m

Restriction maps Sel_m(E/K) into Sel_m(E/L), under the compatibility of the defining fields of WeierstrassCurve.pointRes_mem_shafarevichTateGroup.

theorem WeierstrassCurve.finite_selmerGroup_of_finite_ker_torsionRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {ι : Type u_3} {K' : ι → Type u_4} [(i : ι) → Field (K' i)] [(i : ι) → Algebra K (K' i)] (τK : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (K' i)) {J : Type u_5} {L' : J → Type u_6} [(j : J) → Field (L' j)] [(j : J) → Algebra L (L' j)] (τL : (j : J) → SeparableClosure L →ₐ[L] SeparableClosure (L' j)) (σ : J → ι) [(j : J) → Algebra K (L' j)] [∀ (j : J), IsScalarTower K L (L' j)] [(j : J) → Algebra (K' (σ j)) (L' j)] [∀ (j : J), IsScalarTower K (K' (σ j)) (L' j)] {m : ℕ} (hker : Finite ↥(W.torsionRes τ m).ker) (hL : Finite ↥((W.baseChange L).selmerGroup τL m)) : Finite ↥(W.selmerGroup τK m)

Finiteness of Sel_m(E/L) gives finiteness of Sel_m(E/K) when restriction of H¹(G_K, E(Kˢ)[m]) to L has finite kernel, under the compatibility of the defining fields of WeierstrassCurve.pointRes_mem_shafarevichTateGroup: restriction maps Sel_m(E/K) into the finite group Sel_m(E/L) with finite kernel.