Local Tate duality for elliptic torsion and isogeny kernels

For an elliptic curve over a nonarchimedean local field K, with m invertible in K, cup product along the Weil pairing followed by the local invariant gives a perfect pairing

H¹(K, E[m]) × H¹(K, E[m]) → ℤ/m.

Likewise, for an isogeny φ : E₁ → E₂ over K of degree n invertible in K, cup product along the isogeny Weil pairing e_φ : E₁[φ] × E₂[φ̂] → μ_n (TauCeti.Isogeny.kerCoeffWeilPairing) followed by the local invariant gives a perfect pairing

H¹(K, E₁[φ]) × H¹(K, E₂[φ̂]) → ℤ/n.

Here perfection is stated as bijectivity of the curried map: every additive character of H¹(K, E[m]), respectively of H¹(K, E₂[φ̂]), is pairing with a unique class. This is the finite-coefficient duality used to study annihilators of local Kummer images; for an isogeny it is the local duality between the local conditions of Sel_φ and Sel_φ̂ in Cassels' comparison of these Selmer groups. The image of the Kummer map E(K) → H¹(K, E[m]) is isotropic for the first pairing (WeierstrassCurve.localTateWeilPairing_kummerMap_kummerMap_eq_zero); orthogonality of the Kummer images of an isogeny and of its dual is a further result.

No assumption that K contains the torsion or the roots of unity is required. In mixed characteristic, m and n may be divisible by the residue characteristic.

References

• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, Theorem 2.1.
• J. Silverman, The Arithmetic of Elliptic Curves, X.1 and X.4.
• J. W. S. Cassels, Arithmetic on curves of genus 1. VIII. On conjectures of Birch and Swinnerton-Dyer, J. reine angew. Math. 217 (1965), 180–199.

noncomputable def WeierstrassCurve.localTateWeilPairing {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField 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) →+ ZMod m

Cup product along the Weil pairing followed by the local invariant, valued in ℤ/m.

@[simp]

theorem WeierstrassCurve.localTateWeilPairing_apply {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (a b : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : ((W.localTateWeilPairing m hm) a) b = (TauCeti.ClassFieldTheory.h2MuEquivZMod K hm) ((TauCeti.ClassFieldTheory.muNRepH2Equiv m K) (((W.torsionH1WeilPairing m hm) a) b))

The local pairing is the local invariant of the Weil cup product.

theorem WeierstrassCurve.toRatAddCircle_localTateWeilPairing {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) (a b : TauCeti.ContCohomology.H1 (TauCeti.AbsoluteGaloisGroup K) (W.TorsionCoeff m)) : (ZMod.toRatAddCircle m) (((W.localTateWeilPairing m hm) a) b) = (TauCeti.ClassFieldTheory.invMap K) (((W.torsionWeilBrauerPairing m hm) a) b)

The local Tate pairing, embedded in ℚ/ℤ by k ↦ k/m, is the Brauer invariant of the Weil cup product. The exponent need only be invertible in the field, not in its residue field.

theorem WeierstrassCurve.localTateWeilPairing_bijective {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) : Function.Bijective ⇑(W.localTateWeilPairing m hm)

Perfect local Tate duality for E[m]. Pairing with a class gives a bijection from H¹(K, E[m]) to its additive characters with values in ℤ/m.

theorem WeierstrassCurve.localTateWeilPairing_kummerMap_kummerMap_eq_zero {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) (hm : IsUnit ↑m) [DecidableEq K] (P Q : W.toAffine.Point) : ((W.localTateWeilPairing m hm) ((W.kummerMap m hm) P)) ((W.kummerMap m hm) Q) = 0

The local Kummer image is isotropic for local Tate duality: the local Tate pairing of the Kummer classes of two points of E(K) vanishes.

noncomputable def TauCeti.Isogeny.localTateKerWeilPairing {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (φ : Isogeny W₁.toAffine W₂.toAffine) (hn : IsUnit ↑φ.degree) : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff →+ ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ.dual).KerCoeff →+ ZMod φ.degree

Cup product along the isogeny Weil pairing followed by the local invariant, valued in ℤ/n for n = deg φ.

@[simp]

theorem TauCeti.Isogeny.localTateKerWeilPairing_apply {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (φ : Isogeny W₁.toAffine W₂.toAffine) (hn : IsUnit ↑φ.degree) (a : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff) (b : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ.dual).KerCoeff) : ((φ.localTateKerWeilPairing hn) a) b = (ClassFieldTheory.h2MuEquivZMod K hn) ((ClassFieldTheory.muNRepH2Equiv φ.degree K) (((φ.kerH1WeilPairing hn) a) b))

The local pairing is the local invariant of the isogeny Weil cup product.

theorem TauCeti.Isogeny.localTateKerWeilPairing_explicitCoeff1_torsionCoeffToDualKerCoeff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (φ : Isogeny W₁.toAffine W₂.toAffine) (hn : IsUnit ↑φ.degree) (a : ContCohomology.H1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff) (b : ContCohomology.H1 (AbsoluteGaloisGroup K) (W₁.TorsionCoeff φ.degree)) : ((φ.localTateKerWeilPairing hn) a) ((ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (W₁.TorsionCoeff φ.degree) φ.torsionCoeffToDualKerCoeff ⋯) b) = ((W₁.localTateWeilPairing φ.degree hn) ((ContCohomology.explicitCoeff1 (AbsoluteGaloisGroup K) (Hom.ofIsogeny φ).KerCoeff φ.kerCoeffToTorsionCoeff ⋯) a)) b

The local Tate pairings are compatible with inclusion into degree-torsion and projection onto the dual kernel. No restriction on the residue characteristic is needed.

theorem TauCeti.Isogeny.localTateKerWeilPairing_bijective {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (φ : Isogeny W₁.toAffine W₂.toAffine) (hn : IsUnit ↑φ.degree) : Function.Bijective ⇑(φ.localTateKerWeilPairing hn)

Perfect local Tate duality for the kernels of an isogeny and of its dual. Pairing with a class gives a bijection from H¹(K, E₁[φ]) to the additive characters of H¹(K, E₂[φ̂]) with values in ℤ/n, n = deg φ.