The Weil pairing on first Galois cohomology

For an elliptic curve W over a field K and m invertible in K, the Weil pairing identifies E[m] with its internal dual Hom(E[m], μ_m) as discrete Galois modules. The convention is Q ↦ (P ↦ e_m(P, Q)); no rationality assumption on the torsion or roots of unity is needed.

The resulting cup product pairs two classes of H¹(K, E[m]) into H²(K, μ_m). On cocycles it is (g, h) ↦ e_m(a(g), g • b(h)). This is the pairing used in local duality and in comparing Kummer images with their annihilators.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8 and X.1.
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, §2.

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

The Weil pairing identifies a torsion point with the character P ↦ e_m(P, Q). The internal hom carries the conjugation action, so this is an equivariant map even when Q is not rational.

@[simp]

theorem WeierstrassCurve.toAddMonoidHom_torsionCoeffWeilDual {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (Q : W.TorsionCoeff m) : ((W.torsionCoeffWeilDual m hm) Q).toAddMonoidHom = (W.torsionCoeffWeilPairing m hm).flip Q

Evaluation of the Weil-dual character recovers the Weil pairing.

theorem WeierstrassCurve.torsionCoeffWeilDual_bijective {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : Function.Bijective ⇑(W.torsionCoeffWeilDual m hm)

Self-duality of elliptic torsion as a Galois module. Every character E[m] → μ_m is pairing with a unique point.

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

The cup product along the Weil pairing, with values in H²(K, μ_m). It is obtained from the evaluation duality map by the Weil self-duality of E[m].

theorem WeierstrassCurve.torsionH1WeilPairing_eq_dualityMap1 {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (a b : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : ((W.torsionH1WeilPairing m hm) a) b = ((TauCeti.ContCohomology.dualityMap1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (TauCeti.KummerCoeff K m)) a) ((TauCeti.ContCohomology.explicitCoeff1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.torsionCoeffWeilDual m hm) ⋯) b)

The Weil cup is the evaluation duality map after applying the Weil-dual coefficient map.

theorem WeierstrassCurve.torsionH1WeilPairing_eq_explicitCup11 {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (a b : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : ((W.torsionH1WeilPairing m hm) a) b = ((TauCeti.ContCohomology.explicitCup11 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m) (W.TorsionCoeff m) (TauCeti.KummerCoeff K m) (W.torsionCoeffWeilPairing m hm) ⋯ ⋯) a) b

The pairing is the usual cup product along e_m, in the order e_m(a(g), g • b(h)).