Compatibility of the Weil pairings across levels

Let W be an elliptic curve over a separably closed field F, and let N = m k be a positive integer invertible in F. The Weil pairings at the levels N and m are compatible (Silverman III.8.1(g)):

e_N(S, T) = e_m(k S, T)    for `S ∈ E[N]` and `T ∈ E[m]`,

as roots of unity in F; consequently e_N(S, T) ^ k = e_m(k S, k T) for S, T ∈ E[N]. At N = ℓ ^ (n + 1) and m = ℓ ^ n the second form says that the pairings e_{ℓ ^ n} are compatible with multiplication by ℓ on the torsion tower and the ℓ-th power map on the roots of unity, which is what assembling them into the ℓ-adic Weil pairing on the Tate module requires.

Main results

• TauCeti.Isogeny.coe_weilPairing_eq_coe_weilPairing_nsmul: e_N(S, T) = e_m(k S, T) for S ∈ E[N] and T ∈ E[m].
• TauCeti.Isogeny.coe_weilPairing_pow_eq_coe_weilPairing_nsmul: e_N(S, T) ^ k = e_m(k S, k T) for S, T ∈ E[N].

References

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

theorem TauCeti.Isogeny.instIsIntegrallyClosedCoordinateRingToAffine {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] : IsIntegrallyClosed W.toAffine.CoordinateRing

theorem TauCeti.Isogeny.coe_weilPairing_eq_coe_weilPairing_nsmul {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [DecidableEq F] [IsSepClosed F] {N m : ℕ} [NeZero N] [NeZero m] (hN : ↑N ≠ 0) (hm : ↑m ≠ 0) {k : ℕ} (hk : m * k = N) {S T' : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} {S' T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑m)} (hS : ↑S' = k • ↑S) (hT : ↑T' = ↑T) : ↑(Additive.toMul (((weilPairing W N hN) S) T')) = ↑(Additive.toMul (((weilPairing W m hm) S') T))

The Weil pairings are compatible across levels (Silverman III.8.1(g)): for N = m k invertible in F, e_N(S, T) = e_m(k S, T) for S ∈ E[N] and T ∈ E[m], as roots of unity in F. The m-torsion point k S and the N-torsion point T are given as S' and T'.

theorem TauCeti.Isogeny.coe_weilPairing_pow_eq_coe_weilPairing_nsmul {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [DecidableEq F] [IsSepClosed F] {N m : ℕ} [NeZero N] [NeZero m] (hN : ↑N ≠ 0) (hm : ↑m ≠ 0) {k : ℕ} (hk : m * k = N) {S T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)} {S' T' : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑m)} (hS : ↑S' = k • ↑S) (hT : ↑T' = k • ↑T) : ↑(Additive.toMul (((weilPairing W N hN) S) T)) ^ k = ↑(Additive.toMul (((weilPairing W m hm) S') T'))

The Weil pairings are compatible with the torsion tower: for N = m k invertible in F, e_N(S, T) ^ k = e_m(k S, k T) for S, T ∈ E[N], as roots of unity in F. The m-torsion points k S and k T are given as S' and T'.