Independence of the embeddings of separable closures

For a field extension L/K, restriction on the first Galois cohomology of a Weierstrass curve is independent of the embedding Kˢ → Lˢ. Two embeddings differ by an automorphism of Kˢ; the resulting conjugation of the group map and action on coefficients induce the same cohomology map. Both pointRes and torsionRes are therefore independent of this choice. Consequently, the Shafarevich–Tate and Selmer subgroups defined from any family of extensions are equal for any two families of embeddings.

The coordinate maps themselves do depend on the embedding: the equations pointCoeffBaseChange_comp and torsionCoeffBaseChange_comp describe their transformation.

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.4.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §5.

theorem WeierstrassCurve.pointRes_eq_pointRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ τ' : SeparableClosure K →ₐ[K] SeparableClosure L) : W.pointRes τ = W.pointRes τ'

Restriction on H¹(G_K, E(Kˢ)) is independent of the embedding of separable closures.

theorem WeierstrassCurve.torsionRes_eq_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 : ℕ) : W.torsionRes τ m = W.torsionRes τ' m

Restriction on H¹(G_K, E(Kˢ)[m]) is independent of the embedding of separable closures, for every natural number m.

theorem WeierstrassCurve.shafarevichTateGroup_eq_shafarevichTateGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_3} {F : ι → Type u_4} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (τ τ' : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (F i)) : W.shafarevichTateGroup τ = W.shafarevichTateGroup τ'

The Shafarevich–Tate subgroup relative to a family of field extensions is independent of all choices of embeddings of separable closures.

theorem WeierstrassCurve.selmerGroup_eq_selmerGroup {K : Type u_1} [Field K] (W : WeierstrassCurve K) {ι : Type u_3} {F : ι → Type u_4} [(i : ι) → Field (F i)] [(i : ι) → Algebra K (F i)] (τ τ' : (i : ι) → SeparableClosure K →ₐ[K] SeparableClosure (F i)) (m : ℕ) : W.selmerGroup τ m = W.selmerGroup τ' m

The Selmer subgroup relative to a family of field extensions is independent of all choices of embeddings of separable closures, for every natural number m.