The Weil pairing on the Galois coefficient modules of an elliptic curve

Let W be an elliptic curve over a field K and m a natural number invertible in K. The Weil pairing e_m of W over the separable closure Kˢ is a pairing on the coefficient module E(Kˢ)[m] (WeierstrassCurve.TorsionCoeff) with values in the roots of unity μ_m (TauCeti.KummerCoeff), and it is G_K-equivariant. So a K-rational point T of order dividing m gives a map of discrete G_K-modules

W.weilPairingCoeff m hm T : E(Kˢ)[m] → μ_m,    P ↦ e_m(P, T),

and hence a map H¹(G_K, E[m]) → H¹(G_K, μ_m) into the group which Kummer theory identifies with Kˣ ⧸ (Kˣ)ᵐ (TauCeti.kummerIso). These maps are natural in the field: restriction along a field extension L / K commutes with them, the roots of unity being restricted along the same embedding of separable closures (WeierstrassCurve.explicitMap1_explicitCoeff1_weilPairingCoeff).

When E[m] ⊆ E(K), that is when G_K fixes every point of E(Kˢ)[m], these maps together detect every class: a class of H¹(G_K, E[m]) which dies in H¹(G_K, μ_m) under every weilPairingCoeff T is zero (WeierstrassCurve.explicitCoeff1_weilPairingCoeff_injective). Indeed G_K then acts trivially on μ_m as well, so a class dying in H¹(G_K, μ_m) is a cocycle killed by e_m(·, T), and the Weil pairing is nondegenerate. This is how the Galois cohomology of E[m] over a field containing E[m] is reduced to Kummer theory, the step on which the weak Mordell–Weil theorem and the finiteness of the m-Selmer group rest: over a number field the classes unramified outside a finite set S of places are then controlled by the finite group K(S, m) (Silverman VIII.1.5, VIII.1.6 and X.4.2).

Main definitions

• WeierstrassCurve.torsionCoeffWeilPairing: the Weil pairing E(Kˢ)[m] × E(Kˢ)[m] → μ_m.
• WeierstrassCurve.weilPairingCoeff: for T ∈ E(K)[m], the equivariant map E(Kˢ)[m] → μ_m, P ↦ e_m(P, T).

Main results

• WeierstrassCurve.torsionCoeffWeilPairing_smul: the Weil pairing is G_K-equivariant.
• WeierstrassCurve.torsionCoeffWeilPairing_torsionCoeffBaseChange: the Weil pairing commutes with the maps on torsion and on roots of unity induced by an embedding Kˢ → Lˢ of separable closures.
• WeierstrassCurve.neg_torsionCoeffWeilPairing: interchanging the arguments negates the pairing.
• WeierstrassCurve.torsionCoeffWeilPairing_nondegenerate: the Weil pairing is nondegenerate.
• WeierstrassCurve.torsionCoeffWeilPairing_two_eq_mu2NegOne: the Weil pairing of two distinct points of order two is the nontrivial element of μ₂.
• WeierstrassCurve.torsionCoeffWeilPairing_sum_ite: the Weil pairing of a sum of points of order two with a nonzero point of order two.
• WeierstrassCurve.explicitMap1_explicitCoeff1_weilPairingCoeff: restriction to a field extension commutes with the maps H¹(G, E[m]) → H¹(G, μ_m).
• WeierstrassCurve.explicitCoeff1_weilPairingCoeff_injective: if G_K fixes E(Kˢ)[m], the maps H¹(G_K, E[m]) → H¹(G_K, μ_m) attached to the points of E(K)[m] are jointly injective.
• WeierstrassCurve.finite_of_forall_finite_image_explicitCoeff1_weilPairingCoeff: if G_K fixes E(Kˢ)[m], a set of classes of H¹(G_K, E[m]) with finite images in H¹(G_K, μ_m) is finite.

References

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

The Weil pairing on E(Kˢ)[m]

noncomputable def WeierstrassCurve.torsionCoeffWeilPairing {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : W.TorsionCoeff m →+ W.TorsionCoeff m →+ TauCeti.KummerCoeff K m

The Weil pairing on the coefficient module E(Kˢ)[m], with values in μ_m: the Weil pairing e_m of W over the separable closure Kˢ, for m invertible in K.

theorem WeierstrassCurve.torsionCoeffWeilPairing_apply {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [NeZero m] (hm' : ↑m ≠ 0) (P Q : W.TorsionCoeff m) : ((W.torsionCoeffWeilPairing m hm) P) Q = ((TauCeti.Isogeny.weilPairing (W.baseChange (SeparableClosure K)) m hm') ((W.pointCoeffEquiv.torsionByCongr ↑m).symm P)) ((W.pointCoeffEquiv.torsionByCongr ↑m).symm Q)

torsionCoeffWeilPairing is the Weil pairing of W over Kˢ, read through the identification WeierstrassCurve.pointCoeffEquiv of E(Kˢ) with the points of W⁄Kˢ.

@[simp]

theorem WeierstrassCurve.torsionCoeffWeilPairing_self {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (P : W.TorsionCoeff m) : ((W.torsionCoeffWeilPairing m hm) P) P = 0

The Weil pairing on the coefficient module is alternating (Silverman III.8.1(b)).

theorem WeierstrassCurve.neg_torsionCoeffWeilPairing {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (P Q : W.TorsionCoeff m) : -((W.torsionCoeffWeilPairing m hm) P) Q = ((W.torsionCoeffWeilPairing m hm) Q) P

Interchanging the arguments negates the Weil pairing on the coefficient module.

@[simp]

theorem WeierstrassCurve.torsionCoeffWeilPairing_smul {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (σ : TauCeti.AbsoluteGaloisGroup K) (P Q : W.TorsionCoeff m) : ((W.torsionCoeffWeilPairing m hm) (σ • P)) (σ • Q) = σ • ((W.torsionCoeffWeilPairing m hm) P) Q

The Weil pairing is Galois-equivariant (Silverman III.8.1(e)): e_m(σ P, σ Q) = σ (e_m(P, Q)) for every σ ∈ G_K.

theorem WeierstrassCurve.torsionCoeffWeilPairing_nondegenerate {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) {P : W.TorsionCoeff m} (hP : ∀ (Q : W.TorsionCoeff m), ((W.torsionCoeffWeilPairing m hm) P) Q = 0) : P = 0

The Weil pairing is nondegenerate: if e_m(P, Q) = 1 for every Q ∈ E(Kˢ)[m], then P = O.

theorem WeierstrassCurve.torsionCoeffWeilPairing_two_eq_mu2NegOne {K : Type u_1} [Field K] {W : WeierstrassCurve K} [W.IsElliptic] (h2 : IsUnit ↑2) {T S : W.TorsionCoeff 2} (hT : T ≠ 0) (hS : S ≠ 0) (hTS : T ≠ S) : ((W.torsionCoeffWeilPairing 2 h2) T) S = TauCeti.mu2NegOne

The Weil pairing of two distinct points of order two is -1: on E(Kˢ)[2], for 2 invertible in K, e₂(T, S) is the nontrivial element of μ₂ whenever T and S are distinct and nonzero.

theorem WeierstrassCurve.torsionCoeffWeilPairing_sum_ite {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (h2 : IsUnit ↑2) [Fintype (W.TorsionCoeff 2)] (m : W.TorsionCoeff 2 → TauCeti.KummerCoeff K 2) [DecidablePred fun (x : W.TorsionCoeff 2) => m x = 0] {S : W.TorsionCoeff 2} (hS : S ≠ 0) : ((W.torsionCoeffWeilPairing 2 h2) (∑ T : W.TorsionCoeff 2, if m T = 0 then 0 else T)) S = ∑ T : W.TorsionCoeff 2, m T - m 0 - m S

Pairing with a sum of points of order two. For a family m of square roots of unity indexed by E(Kˢ)[2], the sum of the points T with m T ≠ 0 pairs with a nonzero point S to ∑ T, m T - m O - m S, as two distinct nonzero points of order two pair to -1.

Change of field

theorem WeierstrassCurve.torsionCoeffWeilPairing_torsionCoeffBaseChange {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {m : ℕ} (hm : IsUnit ↑m) {L : Type u_2} [Field L] [Algebra K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) (P Q : W.TorsionCoeff m) : (((W.baseChange L).torsionCoeffWeilPairing m ⋯) ((W.torsionCoeffBaseChange τ m) P)) ((W.torsionCoeffBaseChange τ m) Q) = (TauCeti.kummerCoeffBaseChange m τ) (((W.torsionCoeffWeilPairing m hm) P) Q)

The Weil pairing commutes with change of field (Silverman III.8.1): for an embedding τ : Kˢ → Lˢ over K, e_m(τ P, τ Q) = τ (e_m(P, Q)).

The coefficient map attached to a rational torsion point

noncomputable def WeierstrassCurve.weilPairingCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) : W.TorsionCoeff m →+[TauCeti.AbsoluteGaloisGroup K] TauCeti.KummerCoeff K m

The map E(Kˢ)[m] → μ_m of a rational torsion point: for T ∈ E(K)[m], the G_K-equivariant map P ↦ e_m(P, T). It is equivariant because the Weil pairing is and G_K fixes T.

@[simp]

theorem WeierstrassCurve.weilPairingCoeff_apply {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) (P : W.TorsionCoeff m) : (W.weilPairingCoeff m hm T) P = ((W.torsionCoeffWeilPairing m hm) P) ((W.baseTorsionCoeff m) T)

weilPairingCoeff T is the Weil pairing with the image of T in E(Kˢ)[m].

Restriction to a field extension

theorem WeierstrassCurve.explicitMap1_explicitCoeff1_weilPairingCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] {L : Type u_2} [Field L] [Algebra K L] [DecidableEq L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) {T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)} {T' : ↥(AddSubgroup.torsionBy (W.baseChange L).toAffine.Point ↑m)} (hT : ↑T' = (W.toAffine.pointMap L) ↑T) (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : (TauCeti.ContCohomology.explicitMap1 (TauCeti.AbsoluteGaloisGroup K) (TauCeti.KummerCoeff K m) (TauCeti.AbsoluteGaloisGroup L) (TauCeti.KummerCoeff L m) (TauCeti.absoluteGaloisGroupMap τ) (TauCeti.kummerCoeffBaseChange m τ) ⋯ ⋯) ((TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.weilPairingCoeff m hm T) ⋯) c) = (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup L) ((W.baseChange L).TorsionCoeff m) ((W.baseChange L).weilPairingCoeff m ⋯ T') ⋯) ((W.torsionRes τ m) c)

Restriction commutes with the maps H¹(G, E[m]) → H¹(G, μ_m): for a field extension L / K with an embedding τ : Kˢ → Lˢ over K, and T' ∈ E(L)[m] the image of T ∈ E(K)[m], restricting to G_L and then pairing with T' is pairing with T and then restricting the roots of unity along τ.

Detecting classes when E[m] is rational

theorem WeierstrassCurve.explicitCoeff1_weilPairingCoeff_injective {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] (h : ∀ (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m), σ • P = P) : Function.Injective fun (c : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)) => (TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.weilPairingCoeff m hm T) ⋯) c

The Weil pairing detects H¹(G_K, E[m]) when E[m] ⊆ E(K): if G_K fixes every point of E(Kˢ)[m], then a class of H¹(G_K, E[m]) is determined by its images in H¹(G_K, μ_m) under the maps e_m(·, T) attached to the points T ∈ E(K)[m]. Via the Kummer isomorphism H¹(G_K, μ_m) ≃ Kˣ ⧸ (Kˣ)ᵐ this embeds H¹(G_K, E[m]) into a product of copies of Kˣ ⧸ (Kˣ)ᵐ (Silverman VIII.1 and X.1).

theorem WeierstrassCurve.finite_of_forall_finite_image_explicitCoeff1_weilPairingCoeff {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] (h : ∀ (σ : TauCeti.AbsoluteGaloisGroup K) (P : W.TorsionCoeff m), σ • P = P) {A : Set (TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m))} (hA : ∀ (T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑m)), (⇑(TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.weilPairingCoeff m hm T) ⋯) '' A).Finite) : A.Finite

Finiteness through the Weil pairing: if G_K fixes every point of E(Kˢ)[m], a set of classes of H¹(G_K, E[m]) is finite as soon as, for each T ∈ E(K)[m], its image in H¹(G_K, μ_m) under e_m(·, T) is finite.