Restriction to an embedded extension as restriction to a fixing subgroup

Let W be a Weierstrass curve over a field K and L/K an extension embedded in Kˢ by σ : L →ₐ[K] Kˢ. Then Kˢ is a separable closure of L, and G_L is identified with the subgroup Gal(Kˢ/σ(L)) of G_K fixing σ(L) pointwise (TauCeti.absoluteGaloisGroupEquivFixingSubgroup). Restriction of the Galois cohomology of W to L, defined along an embedding of separable closures τ : Kˢ → Lˢ (WeierstrassCurve.pointRes, WeierstrassCurve.torsionRes), is therefore the group-theoretic restriction to Gal(Kˢ/σ(L)) followed by an isomorphism. In particular the two restrictions have the same kernel (WeierstrassCurve.ker_pointRes, WeierstrassCurve.ker_torsionRes), by TauCeti.ContCohomology.explicitMap1_eq_zero_iff_explicitRes1_eq_zero applied to the bijective coordinate maps WeierstrassCurve.pointCoeffBaseChange_bijective and WeierstrassCurve.torsionCoeffBaseChange_bijective.

For the m-division field L = K(E[m]) of an elliptic curve and m ≠ 0, the kernel of group-theoretic restriction is finite by inflation-restriction (WeierstrassCurve.finite_ker_explicitRes1_divisionField), so the restriction H¹(G_K, E[m]) → H¹(G_L, E[m]) has finite kernel (WeierstrassCurve.finite_ker_torsionRes_divisionField). Since restriction also maps Sel_m(E/K) into Sel_m(E/K(E[m])), the finiteness of Sel_m(E/K) follows from that of Sel_m(E/K(E[m])) (WeierstrassCurve.finite_selmerGroup_of_finite_selmerGroup_divisionField). This is the step of the proof of the finiteness of the m-Selmer group (Silverman X.4.2) that replaces K by K(E[m]), over which E[m] is rational.

Main results

• WeierstrassCurve.pointRes_eq_zero_iff, WeierstrassCurve.torsionRes_eq_zero_iff: a class restricts to zero over L exactly when it restricts to zero on Gal(Kˢ/σ(L)).
• WeierstrassCurve.ker_pointRes, WeierstrassCurve.ker_torsionRes: the same statement for the kernels.
• WeierstrassCurve.forall_smul_eq_torsionCoeff_divisionField: over the m-division field, every point of E[m] is rational.
• WeierstrassCurve.finite_ker_torsionRes_divisionField: for W elliptic and m ≠ 0, restriction of H¹(G_K, E[m]) to the m-division field has finite kernel.
• WeierstrassCurve.finite_selmerGroup_of_finite_selmerGroup_divisionField: hence Sel_m(E/K) is finite once Sel_m(E/K(E[m])) is.

References

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

Restriction to the fixing subgroup

theorem WeierstrassCurve.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) (σ : L →ₐ[K] SeparableClosure K) {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff} : (W.pointRes τ) c = 0 ↔ (TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff σ.fieldRange.fixingSubgroup) c = 0

A class of H¹(G_K, E(Kˢ)) restricts to zero over L exactly when it restricts to zero on the subgroup Gal(Kˢ/σ(L)) of G_K.

theorem WeierstrassCurve.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) (σ : L →ₐ[K] SeparableClosure K) {m : ℕ} {c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)} : (W.torsionRes τ m) c = 0 ↔ (TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) σ.fieldRange.fixingSubgroup) c = 0

A class of H¹(G_K, E(Kˢ)[m]) restricts to zero over L exactly when it restricts to zero on the subgroup Gal(Kˢ/σ(L)) of G_K.

theorem WeierstrassCurve.ker_pointRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (σ : L →ₐ[K] SeparableClosure K) : (W.pointRes τ).ker = (TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff σ.fieldRange.fixingSubgroup).ker

Restriction of H¹(G_K, E(Kˢ)) to L has the kernel of restriction to Gal(Kˢ/σ(L)).

theorem WeierstrassCurve.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) (σ : L →ₐ[K] SeparableClosure K) (m : ℕ) : (W.torsionRes τ m).ker = (TauCeti.ContCohomology.explicitRes1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) σ.fieldRange.fixingSubgroup).ker

Restriction of H¹(G_K, E(Kˢ)[m]) to L has the kernel of restriction to Gal(Kˢ/σ(L)).

Restriction to the division field

theorem WeierstrassCurve.forall_smul_eq_torsionCoeff_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) (m : ℕ) (g : TauCeti.AbsoluteGaloisGroup ↥(W.divisionField m)) (P : (W.baseChange ↥(W.divisionField m)).TorsionCoeff m) : g • P = P

Over the m-division field K(E[m]), every geometric m-torsion point is rational: G_L acts trivially on E(Lˢ)[m] for L = K(E[m]).

theorem WeierstrassCurve.finite_ker_torsionRes_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) [NeZero m] (τ : SeparableClosure K →ₐ[K] SeparableClosure ↥(W.divisionField m)) : Finite ↥(W.torsionRes τ m).ker

Restriction of H¹(G_K, E[m]) to the m-division field K(E[m]) has finite kernel, for W elliptic and m ≠ 0, along any embedding of separable closures.

theorem WeierstrassCurve.finite_selmerGroup_of_finite_selmerGroup_divisionField {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) [NeZero m] {ι : 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 (↥(W.divisionField m)) (L' j)] (τL : (j : J) → SeparableClosure ↥(W.divisionField m) →ₐ[↥(W.divisionField m)] SeparableClosure (L' j)) (σ : J → ι) [(j : J) → Algebra K (L' j)] [∀ (j : J), IsScalarTower K (↥(W.divisionField m)) (L' j)] [(j : J) → Algebra (K' (σ j)) (L' j)] [∀ (j : J), IsScalarTower K (K' (σ j)) (L' j)] (h : Finite ↥((W.baseChange ↥(W.divisionField m)).selmerGroup τL m)) : Finite ↥(W.selmerGroup τK m)

The finiteness of Sel_m(E/K) reduces to the finiteness of Sel_m(E/K(E[m])), for W elliptic and m ≠ 0: if each field L' j defining the Selmer group over the m-division field K(E[m]) is an extension of the field K' (σ j) defining that over K, compatibly with K → K(E[m]) → L' j, and Sel_m(E/K(E[m])) is finite, then so is Sel_m(E/K).