The Weil pairing as a ZMod N-bilinear form

Let W be an elliptic curve over a separably closed field F and N a positive integer invertible in F. Both E[N] and μ_N, written additively, are killed by N, so they are ZMod N-modules, and the Weil pairing e_N, being additive in each variable, is ZMod N-linear in each variable. This file records that linearity and packages e_N as a ZMod N-bilinear form on E[N], which is alternating and left-separating. This is the form in which linear algebra over ZMod N applies to the Weil pairing.

The pairing is defined on Submodule.torsionBy ℤ, while the ZMod N-module structure is on AddSubgroup.torsionBy, the same subtype of points. The statements here are made on the latter, so that c • S is the ZMod N-action.

Main definitions

• TauCeti.Isogeny.weilPairingBilin: the Weil pairing as a ZMod N-bilinear form on E[N].

Main results

• TauCeti.Isogeny.weilPairing_zmod_smul_left and TauCeti.Isogeny.weilPairing_zmod_smul_right: e_N is ZMod N-linear in each variable.
• TauCeti.Isogeny.isAlt_weilPairingBilin: the form is alternating.
• TauCeti.Isogeny.separatingLeft_weilPairingBilin: the form is left-separating.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.1.

theorem TauCeti.Isogeny.weilPairing_zmod_smul_left {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (c : ZMod N) (S T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N)) : ((weilPairing W N hN) (c • S)) T = c • ((weilPairing W N hN) S) T

The Weil pairing is ZMod N-linear in its first variable.

theorem TauCeti.Isogeny.weilPairing_zmod_smul_right {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (c : ZMod N) (S T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N)) : ((weilPairing W N hN) S) (c • T) = c • ((weilPairing W N hN) S) T

The Weil pairing is ZMod N-linear in its second variable.

noncomputable def TauCeti.Isogeny.weilPairingBilin {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N) →ₗ[ZMod N] ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N) →ₗ[ZMod N] Additive ↥(rootsOfUnity N F)

The Weil pairing as a ZMod N-bilinear form on E[N], over a separably closed field in which N is invertible.

@[simp]

theorem TauCeti.Isogeny.weilPairingBilin_apply {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (S T : ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N)) : ((weilPairingBilin W N hN) S) T = ((weilPairing W N hN) S) T

The bilinear form weilPairingBilin evaluates to the Weil pairing.

theorem TauCeti.Isogeny.isAlt_weilPairingBilin {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : (weilPairingBilin W N hN).IsAlt

The Weil pairing, as a ZMod N-bilinear form, is alternating.

theorem TauCeti.Isogeny.separatingLeft_weilPairingBilin {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : (weilPairingBilin W N hN).SeparatingLeft

The Weil pairing, as a ZMod N-bilinear form, is left-separating.