Restriction of the Galois cohomology of an elliptic curve along a field extension

Let W be a Weierstrass curve over a field K, let L/K be an arbitrary field extension, and let τ : Kˢ →ₐ[K] Lˢ be a K-embedding of separable closures. Applying τ to coordinates maps the points of W over Kˢ to the points of W⁄L over Lˢ,

W.pointCoeffBaseChange τ : E(Kˢ) → E(Lˢ),

and this map is equivariant along the induced map of absolute Galois groups TauCeti.absoluteGaloisGroupMap τ : G_L → G_K (WeierstrassCurve.pointCoeffBaseChange_smul). It therefore induces restriction maps

W.pointRes τ : H¹(G_K, E(Kˢ)) → H¹(G_L, E(Lˢ)),
W.torsionRes τ m : H¹(G_K, E(Kˢ)[m]) → H¹(G_L, E(Lˢ)[m]),

which commute with the map induced by the inclusion E[m] → E (WeierstrassCurve.pointRes_torsionCoeffIncl). When L is a completion K_v of a global field, these are the localisation maps at v, out of which the Selmer and Shafarevich–Tate groups are cut.

The group and coordinate maps depend on τ, but their induced cohomology maps do not: pointRes_eq_pointRes and torsionRes_eq_torsionRes in TauCeti/AlgebraicGeometry/EllipticCurve/GaloisCohomology/EmbeddingIndependence.lean prove independence of this choice.

The main result is that restriction is compatible with the Kummer maps (WeierstrassCurve.torsionRes_kummerMap): the restriction of the Kummer class of P ∈ E(K) is the Kummer class over L of the image of P in E(L). This is what lets the image of a local Kummer map serve as the local condition at L of the m-Selmer group.

Main definitions

• WeierstrassCurve.pointCoeffBaseChange: the equivariant map E(Kˢ) → E(Lˢ) along τ.
• WeierstrassCurve.torsionCoeffBaseChange: its restriction E(Kˢ)[m] → E(Lˢ)[m].
• WeierstrassCurve.pointRes: restriction H¹(G_K, E(Kˢ)) → H¹(G_L, E(Lˢ)).
• WeierstrassCurve.torsionRes: restriction H¹(G_K, E(Kˢ)[m]) → H¹(G_L, E(Lˢ)[m]).

Main results

• WeierstrassCurve.pointCoeffBaseChange_smul: pointCoeffBaseChange τ is equivariant along absoluteGaloisGroupMap τ.
• WeierstrassCurve.pointCoeffBaseChange_pointCoeffEquiv: it is Mathlib's point map along τ.
• WeierstrassCurve.pointCoeffBaseChange_basePointCoeff: on points of E(K) it is base change to L.
• WeierstrassCurve.pointCoeffBaseChange_pointCoeffBaseChange, WeierstrassCurve.torsionCoeffBaseChange_torsionCoeffBaseChange: the maps compose in a tower K → L → M, up to the identification of (W⁄L)⁄M with W⁄M.
• WeierstrassCurve.pointCoeffBaseChange_bijective, WeierstrassCurve.torsionCoeffBaseChange_bijective: the coordinate maps along a bijective embedding of separable closures are bijective.
• WeierstrassCurve.forall_smul_eq_torsionCoeff_baseChange: along a bijective embedding, G_L acts trivially on E(Lˢ)[m] once it acts trivially on E(Kˢ)[m].
• WeierstrassCurve.pointRes_torsionCoeffIncl: restriction commutes with H¹(G, E[m]) → H¹(G, E).
• WeierstrassCurve.torsionRes_kummerMap: restriction commutes with the Kummer maps.

Implementation notes

The restriction maps follow the pullback of the Kummer classes of the multiplicative group along an arbitrary field extension, TauCeti.kummerCoeffBaseChange and TauCeti.explicitMap1_kummerMap in TauCeti/FieldTheory/GaloisCohomology/Kummer.lean.

References

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

The map on points over the separable closures

theorem WeierstrassCurve.nonsingular_baseChange_separableClosure {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {x y : SeparableClosure K} (h : (W.baseChange (SeparableClosure K)).toAffine.Nonsingular x y) : ((W.baseChange L).baseChange (SeparableClosure L)).toAffine.Nonsingular (τ x) (τ y)

Applying τ to the coordinates of a nonsingular point of W over Kˢ gives a nonsingular point of W⁄L over Lˢ.

noncomputable def WeierstrassCurve.pointCoeffBaseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) : W.PointCoeff →+ (W.baseChange L).PointCoeff

The map E(Kˢ) → E(Lˢ) along an embedding τ : Kˢ →ₐ[K] Lˢ of separable closures: it applies τ to the coordinates of a point.

theorem WeierstrassCurve.pointCoeffBaseChange_pointCoeffEquiv {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (P : (W.baseChange (SeparableClosure K)).toAffine.Point) : (W.pointCoeffBaseChange τ) (W.pointCoeffEquiv P) = (W.baseChange L).pointCoeffEquiv ((AddEquiv.cast ⋯) ((Affine.Point.map τ) P))

pointCoeffBaseChange τ is Mathlib's point map along τ, read on W⁄L through the identification of W⁄Lˢ with (W⁄L)⁄Lˢ.

@[simp]

theorem WeierstrassCurve.pointCoeffBaseChange_pointCoeffEquiv_some {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {x y : SeparableClosure K} (h : (W.baseChange (SeparableClosure K)).toAffine.Nonsingular x y) : (W.pointCoeffBaseChange τ) (W.pointCoeffEquiv (Affine.Point.some x y h)) = (W.baseChange L).pointCoeffEquiv (Affine.Point.some (τ x) (τ y) ⋯)

pointCoeffBaseChange τ applies τ to both coordinates of an affine point.

@[simp]

theorem WeierstrassCurve.pointCoeffBaseChange_smul {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (g : TauCeti.AbsoluteGaloisGroup L) (P : W.PointCoeff) : (W.pointCoeffBaseChange τ) ((TauCeti.absoluteGaloisGroupMap τ) g • P) = g • (W.pointCoeffBaseChange τ) P

pointCoeffBaseChange τ is equivariant along absoluteGaloisGroupMap τ : G_L → G_K.

theorem WeierstrassCurve.pointCoeffBaseChange_comp {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.PointCoeff) : (W.pointCoeffBaseChange (τ.comp ↑σ)) P = (W.pointCoeffBaseChange τ) (σ • P)

Precomposing an embedding by a Galois automorphism composes the coordinate map with the same automorphism's action on points.

@[simp]

theorem WeierstrassCurve.pointCoeffBaseChange_basePointCoeff {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) [DecidableEq K] [DecidableEq L] (P : W.toAffine.Point) : (W.pointCoeffBaseChange τ) (W.basePointCoeff P) = (W.baseChange L).basePointCoeff ((W.toAffine.pointMap L) P)

On points of E(K), pointCoeffBaseChange τ is base change to L: the image in E(Lˢ) of a point of E(K) is the image of its base change in E(L).

The map on m-torsion

noncomputable def WeierstrassCurve.torsionCoeffBaseChange {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.TorsionCoeff m →+ (W.baseChange L).TorsionCoeff m

The map E(Kˢ)[m] → E(Lˢ)[m] along τ, the restriction of pointCoeffBaseChange τ.

@[simp]

theorem WeierstrassCurve.coe_torsionCoeffBaseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (m : ℕ) (P : W.TorsionCoeff m) : ↑((W.torsionCoeffBaseChange τ m) P) = (W.pointCoeffBaseChange τ) ↑P

@[simp]

theorem WeierstrassCurve.torsionCoeffBaseChange_smul {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (m : ℕ) (g : TauCeti.AbsoluteGaloisGroup L) (P : W.TorsionCoeff m) : (W.torsionCoeffBaseChange τ m) ((TauCeti.absoluteGaloisGroupMap τ) g • P) = g • (W.torsionCoeffBaseChange τ m) P

torsionCoeffBaseChange τ m is equivariant along absoluteGaloisGroupMap τ : G_L → G_K.

theorem WeierstrassCurve.torsionCoeffBaseChange_comp {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (σ : TauCeti.AbsoluteGaloisGroup K) (m : ℕ) (P : W.TorsionCoeff m) : (W.torsionCoeffBaseChange (τ.comp ↑σ) m) P = (W.torsionCoeffBaseChange τ m) (σ • P)

Precomposing an embedding by a Galois automorphism composes its map on torsion points with the same automorphism's action.

Bijectivity along a bijective embedding

theorem WeierstrassCurve.pointCoeffBaseChange_bijective {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) {τ : SeparableClosure K →ₐ[K] SeparableClosure L} (hτ : Function.Bijective ⇑τ) : Function.Bijective ⇑(W.pointCoeffBaseChange τ)

Along a bijective embedding of separable closures, E(Kˢ) → E(Lˢ) is bijective.

theorem WeierstrassCurve.torsionCoeffBaseChange_bijective {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) {τ : SeparableClosure K →ₐ[K] SeparableClosure L} (m : ℕ) (hτ : Function.Bijective ⇑τ) : Function.Bijective ⇑(W.torsionCoeffBaseChange τ m)

Along a bijective embedding of separable closures, E(Kˢ)[m] → E(Lˢ)[m] is bijective.

theorem WeierstrassCurve.forall_smul_eq_torsionCoeff_baseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) {τ : SeparableClosure K →ₐ[K] SeparableClosure L} (m : ℕ) (hτ : Function.Bijective ⇑τ) (h : ∀ (g : TauCeti.AbsoluteGaloisGroup L) (Q : W.TorsionCoeff m), (TauCeti.absoluteGaloisGroupMap τ) g • Q = Q) (g : TauCeti.AbsoluteGaloisGroup L) (P : (W.baseChange L).TorsionCoeff m) : g • P = P

Rational m-torsion descends along a bijective embedding of separable closures: if G_L acts trivially on E(Kˢ)[m] through absoluteGaloisGroupMap τ, then it acts trivially on E(Lˢ)[m].

Towers of extensions

The identification of (W⁄L)⁄M with W⁄M is Mathlib's WeierstrassCurve.map_baseChange at IsScalarTower.toAlgHom K L M, whose underlying ring homomorphism is algebraMap L M; the show in the statements below only restates it in terms of base change.

theorem WeierstrassCurve.pointCoeffBaseChange_pointCoeffBaseChange {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) (hτ : ∀ (x : SeparableClosure K), τ'' x = τ' (τ x)) (P : W.PointCoeff) : ((W.baseChange L).pointCoeffBaseChange τ') ((W.pointCoeffBaseChange τ) P) = (AddEquiv.cast ⋯) ((W.pointCoeffBaseChange τ'') P)

The coordinate maps compose in a tower K → L → M: if τ'' : Kˢ → Mˢ is the composite of τ : Kˢ → Lˢ and τ' : Lˢ → Mˢ, mapping E(Kˢ) → E(Lˢ) → E(Mˢ) along τ and τ' is mapping along τ'', followed by the identification of (W⁄L)⁄M with W⁄M.

theorem WeierstrassCurve.torsionCoeffBaseChange_torsionCoeffBaseChange {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) (hτ : ∀ (x : SeparableClosure K), τ'' x = τ' (τ x)) (m : ℕ) (P : W.TorsionCoeff m) : ((W.baseChange L).torsionCoeffBaseChange τ' m) ((W.torsionCoeffBaseChange τ m) P) = (AddEquiv.cast ⋯) ((W.torsionCoeffBaseChange τ'' m) P)

The maps on m-torsion compose in a tower K → L → M, as in WeierstrassCurve.pointCoeffBaseChange_pointCoeffBaseChange.

Restriction on first cohomology

noncomputable def WeierstrassCurve.pointRes {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff →+ TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup L) (W.baseChange L).PointCoeff

Restriction H¹(G_K, E(Kˢ)) → H¹(G_L, E(Lˢ)) along τ: pullback along the compatible pair (absoluteGaloisGroupMap τ, pointCoeffBaseChange τ).

theorem WeierstrassCurve.pointRes_eq_explicitMap1 {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 τ = TauCeti.ContCohomology.explicitMap1 (TauCeti.AbsoluteGaloisGroup K) W.PointCoeff (TauCeti.AbsoluteGaloisGroup L) (W.baseChange L).PointCoeff (TauCeti.absoluteGaloisGroupMap τ) (W.pointCoeffBaseChange τ) ⋯ ⋯

pointRes τ is the pullback along (absoluteGaloisGroupMap τ, pointCoeffBaseChange τ).

noncomputable def WeierstrassCurve.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 : ℕ) : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) →+ TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup L) ((W.baseChange L).TorsionCoeff m)

Restriction H¹(G_K, E(Kˢ)[m]) → H¹(G_L, E(Lˢ)[m]) along τ: pullback along the compatible pair (absoluteGaloisGroupMap τ, torsionCoeffBaseChange τ m).

theorem WeierstrassCurve.torsionRes_eq_explicitMap1 {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 = TauCeti.ContCohomology.explicitMap1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (TauCeti.AbsoluteGaloisGroup L) ((W.baseChange L).TorsionCoeff m) (TauCeti.absoluteGaloisGroupMap τ) (W.torsionCoeffBaseChange τ m) ⋯ ⋯

torsionRes τ m is the pullback along (absoluteGaloisGroupMap τ, torsionCoeffBaseChange τ m).

@[simp]

theorem WeierstrassCurve.pointRes_torsionCoeffIncl {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (m : ℕ) (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : (W.pointRes τ) ((TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffIncl m) ⋯) c) = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup L) ((W.baseChange L).TorsionCoeff m) ((W.baseChange L).torsionCoeffIncl m) ⋯) ((W.torsionRes τ m) c)

Restriction commutes with H¹(G, E[m]) → H¹(G, E), the map induced by the inclusion E[m] → E.

Compatibility with the Kummer maps

theorem WeierstrassCurve.torsionRes_kummerMap {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (W : WeierstrassCurve K) (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {m : ℕ} [DecidableEq K] [DecidableEq L] [W.IsElliptic] (hm : IsUnit ↑m) (P : W.toAffine.Point) : (W.torsionRes τ m) ((W.kummerMap m hm) P) = ((W.baseChange L).kummerMap m ⋯) ((W.toAffine.pointMap L) P)

Restriction carries Kummer classes to Kummer classes: the restriction to L of the Kummer class of P ∈ E(K) is the Kummer class of the image of P in E(L).