The Weil pairing under change of field

Let W be an elliptic curve over a field F, let f : F →+* K be a homomorphism of fields, and let N be invertible in F. A point P of W is carried to the point f P of W.map f, and this restricts to a homomorphism E[N](F) → E[N](K) (WeierstrassCurve.torsionMapAlong). When F and K are separably closed both groups have N² elements, so it is an isomorphism (WeierstrassCurve.torsionMapAlong_bijective). This file proves that the Weil pairing is functorial under change of field (Silverman III.8.1):

e_N(f S, f T) = f (e_N(S, T)).

The proof follows the definition of the pairing. Let g be a function on W with divisor [N]^* (T) - [N]^* (O). This divisor is supported on the F-rational points of [N]-preimages of T and of O, and the divisor of a function supported on rational points is carried along f point by point (WeierstrassCurve.Affine.FunctionField.principal_map_eq_pushforward). Since f maps the [N]-preimages of T and of O over F bijectively onto those over K, the image f^* g has divisor [N]^* (f T) - [N]^* (O). As f^* intertwines translation by S with translation by f S,

e_N(f S, f T) = τ_{f S} (f^* g) / f^* g = f^* (τ_S g / g) = f (e_N(S, T)).

Main results

• WeierstrassCurve.principal_map_eq_weilPairingDivisor: the image along f of a function with divisor [N]^* (T) - [N]^* (O) has divisor [N]^* (f T) - [N]^* (O).
• WeierstrassCurve.weilPairing_torsionMapAlong: the Weil pairing is functorial under change of field.
• WeierstrassCurve.weilPairing_torsionByCongr_cast: the Weil pairing is unchanged when the curve is transported along an equality.

References

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

theorem WeierstrassCurve.principal_map_eq_weilPairingDivisor {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq F] (W : WeierstrassCurve F) (f : F →+* K) [W.IsElliptic] [IsSepClosed F] [IsSepClosed K] {n : ℤ} (hchar : ↑n ≠ 0) {T : W.toAffine.Point} (hT : n • T = 0) {hψ : TauCeti.Isogeny.psiFunctionField W n ≠ 0} {hψ' : TauCeti.Isogeny.psiFunctionField (W.map f) n ≠ 0} {g : W.toAffine.FunctionFieldˣ} (hg : TauCeti.Divisor.principal ⋯ g = TauCeti.Isogeny.weilPairingDivisor W hψ T) : TauCeti.Divisor.principal ⋯ ((Units.map ↑(Affine.FunctionField.map W.toAffine f)) g) = TauCeti.Isogeny.weilPairingDivisor (W.map f) hψ' (Affine.Point.mapAlong f ⋯ T)

The divisor [n]^* (T) - [n]^* (O) is carried along f: if g is a function on W with that divisor, then its image on W.map f has divisor [n]^* (f T) - [n]^* (O), for an n-torsion point T and n invertible.

@[simp]

theorem WeierstrassCurve.weilPairing_torsionMapAlong {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq F] [DecidableEq K] (W : WeierstrassCurve F) (f : F →+* K) [W.IsElliptic] [IsSepClosed F] [IsSepClosed K] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (S T : ↥(Submodule.torsionBy ℤ W.toAffine.Point ↑N)) : ((TauCeti.Isogeny.weilPairing (W.map f) N ⋯) ((W.torsionMapAlong f ↑N) S)) ((W.torsionMapAlong f ↑N) T) = Additive.ofMul ((restrictRootsOfUnity f N) (Additive.toMul (((TauCeti.Isogeny.weilPairing W N hN) S) T)))

The Weil pairing is functorial under change of field (Silverman III.8.1): for a homomorphism f of separably closed fields and N invertible, e_N(f S, f T) = f (e_N(S, T)).

theorem WeierstrassCurve.weilPairing_torsionByCongr_cast {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {V₁ V₂ : WeierstrassCurve F} [V₁.IsElliptic] [V₂.IsElliptic] (h : V₁ = V₂) (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (P Q : ↥(Submodule.torsionBy ℤ V₁.toAffine.Point ↑N)) : ((TauCeti.Isogeny.weilPairing V₂ N hN) (((AddEquiv.cast h).torsionByCongr ↑N) P)) (((AddEquiv.cast h).torsionByCongr ↑N) Q) = ((TauCeti.Isogeny.weilPairing V₁ N hN) P) Q

The Weil pairing of a Weierstrass curve is unchanged when the curve is transported along an equality, the torsion points being transported with it.