The Brauer-valued Weil cup product

Composing the Weil cup product with H²(K, μ_m) → Br K gives a bilinear pairing on H¹(K, E[m]) over any field. Its comparison with the local Tate pairing is proved in WeilPairing.Local; this module does not require local-field hypotheses.

References

• J. S. Milne, Arithmetic Duality Theorems, second edition, I, §§2 and 4.

noncomputable def WeierstrassCurve.torsionWeilBrauerPairing {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.ClassFieldTheory.Br K

The Weil cup product, followed by the inclusion H²(K, μ_m) → Br K. It is bilinear on the first cohomology of elliptic torsion.

@[simp]

theorem WeierstrassCurve.torsionWeilBrauerPairing_apply {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.torsionWeilBrauerPairing m hm) a) b = (TauCeti.ClassFieldTheory.h2MuToBr m K) ((TauCeti.ClassFieldTheory.muNRepH2Equiv m K) (((W.torsionH1WeilPairing m hm) a) b))

The Brauer-valued pairing is the image of the Weil cup product.