The Weil pairing takes primitive values

Let W be an elliptic curve over a separably closed field F and N a positive integer invertible in F. The Weil pairing e_N on E[N] takes a primitive N-th root of unity as a value (Silverman III.8.1.1). In a basis (P, Q) of E[N] over ZMod N, bilinearity and the alternating property give e_N(P, a • P + c • Q) = c • e_N(P, Q), so if r • e_N(P, Q) = 0 then r • P pairs trivially with all of E[N], and nondegeneracy forces r = 0. Hence e_N(P, Q) is a primitive N-th root of unity, and e_N(P, ·) maps E[N] onto μ_N.

Combined with Galois equivariance, e_N(σ S, σ T) = σ (e_N(S, T)), this shows that over any field F, with K a separably closed extension, an F-automorphism of K acting trivially on E[N] fixes every N-th root of unity in K. When K is Galois over F, for instance a separable closure, and the Galois action on E[N] is trivial, F itself contains a primitive N-th root of unity: if E[N] ⊆ E(F) then μ_N ⊆ F. Over a field containing E[N], both E[N] and μ_N are then trivial Galois modules, so E[N] ≅ μ_N × μ_N; this is how Kummer theory enters the weak Mordell–Weil theorem and the finiteness of the N-Selmer group (Silverman VIII.1.2 and X.4.2).

Main results

• TauCeti.Isogeny.exists_isPrimitiveRoot_weilPairing: some value e_N(S, T) is a primitive N-th root of unity.
• TauCeti.Isogeny.exists_surjective_weilPairing: for some S, the map e_N(S, ·) is onto μ_N.
• WeierstrassCurve.algEquiv_apply_eq_self_of_torsionGaloisAction_eq_one: an automorphism acting trivially on E[N] fixes the N-th roots of unity.
• WeierstrassCurve.exists_isPrimitiveRoot_of_forall_torsionGaloisAction_eq_one: if the Galois action on E[N] is trivial, the base field contains a primitive N-th root of unity.
• WeierstrassCurve.exists_isPrimitiveRoot_of_natCard_torsionBy: if E(F) has N² points of order dividing N, that is E[N] ⊆ E(F), then F contains a primitive N-th root of unity.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.1.1, VIII.1.2 and X.4.2.

theorem TauCeti.Isogeny.exists_isPrimitiveRoot_weilPairing {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : ∃ (S : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)) (T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)), IsPrimitiveRoot (↑↑(Additive.toMul (((weilPairing W N hN) S) T))) N

The Weil pairing takes a primitive N-th root of unity as a value (Silverman III.8.1.1), over a separably closed field in which N is invertible.

theorem TauCeti.Isogeny.exists_surjective_weilPairing {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : ∃ (S : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)), Function.Surjective ⇑((weilPairing W N hN) S)

The Weil pairing is onto μ_N in its second variable for a suitable first argument, over a separably closed field in which N is invertible.

theorem WeierstrassCurve.algEquiv_apply_eq_self_of_torsionGaloisAction_eq_one {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {N : ℕ} [NeZero N] {K : Type u_2} [Field K] [DecidableEq K] [Algebra F K] [IsSepClosed K] (hN : ↑N ≠ 0) {σ : Gal(K/F)} (hσ : (W.torsionGaloisAction ↑N) σ = 1) {ζ : K} (hζ : ζ ^ N = 1) : σ ζ = ζ

An automorphism acting trivially on E[N] fixes the N-th roots of unity: for an F-automorphism σ of a separably closed field K in which N is invertible, if σ fixes every N-torsion point of W over K, then σ ζ = ζ for every ζ ∈ K with ζ ^ N = 1.

theorem WeierstrassCurve.exists_isPrimitiveRoot_of_forall_torsionGaloisAction_eq_one {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {N : ℕ} [NeZero N] {K : Type u_2} [Field K] [DecidableEq K] [Algebra F K] [IsSepClosed K] (hN : ↑N ≠ 0) [IsGalois F K] (h : ∀ (σ : Gal(K/F)), (W.torsionGaloisAction ↑N) σ = 1) : ∃ (ζ : F), IsPrimitiveRoot ζ N

If the Galois action on E[N] is trivial, the base field contains a primitive N-th root of unity (Silverman III.8.1.1): for a separably closed Galois extension K of F, such as a separable closure, in which N is invertible, if every F-automorphism of K fixes the N-torsion of W over K, then F contains a primitive N-th root of unity.

theorem WeierstrassCurve.exists_isPrimitiveRoot_of_natCard_torsionBy {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {N : ℕ} [NeZero N] [DecidableEq F] (hN : ↑N ≠ 0) (h : Nat.card ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N) = N ^ 2) : ∃ (ζ : F), IsPrimitiveRoot ζ N

If E[N] ⊆ E(F) then μ_N ⊆ F (Silverman III.8.1.1): if an elliptic curve over F has N² rational N-torsion points, with N invertible in F, then F contains a primitive N-th root of unity.