Galois equivariance of the Weil pairing

Let W be an elliptic curve over a field F, let K be a separably closed extension of F, and let N be a positive integer invertible in K. Every F-automorphism σ of K acts on the points of W over K (WeierstrassCurve.pointGaloisAction), on its function field (WeierstrassCurve.functionFieldGaloisAction) and on its divisors (WeierstrassCurve.divisorGaloisAction). This file proves that the Weil pairing of W over K commutes with these actions:

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

The proof is Silverman's. The divisor [N]^* (T) - [N]^* (O) is the formal sum of the fibre of [N] over T minus that over O, and σ carries the fibre of [N] over T bijectively onto the fibre over σ T, because it acts on points by a group automorphism. So σ carries the divisor attached to T to the divisor attached to σ T (WeierstrassCurve.divisorGaloisAction_weilPairingDivisor). If g has divisor [N]^* (T) - [N]^* (O), then σ g therefore has divisor [N]^* (σ T) - [N]^* (O), and since σ intertwines translation by S with translation by σ S,

e_N(σ S, σ T) = τ_{σ S} (σ g) / σ g = σ (τ_S g / g) = σ (e_N(S, T)).

Main results

• WeierstrassCurve.divisorGaloisAction_divisorPullback_mulByIntIsogeny_ofPoint: the pullback [n]^* (T) is Galois-equivariant in T.
• WeierstrassCurve.divisorGaloisAction_weilPairingDivisor: the divisor [n]^* (T) - [n]^* (O) is Galois-equivariant in T.
• WeierstrassCurve.weilPairing_torsionGaloisAction: the Weil pairing is Galois-equivariant.

References

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

theorem WeierstrassCurve.divisorGaloisAction_divisorPullback_mulByIntIsogeny_ofPoint {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] [IsSepClosed K] (W : WeierstrassCurve F) [W.IsElliptic] (σ : Gal(K/F)) {n : ℤ} (hchar : ↑n ≠ 0) (T : (toAffine (Affine.baseChange W K)).Point) : (Multiplicative.toAdd (W.divisorGaloisAction σ)) (((TauCeti.Isogeny.mulByIntIsogeny (Affine.baseChange W K) ⋯).divisorPullback ⋯) (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑((toAffine (Affine.baseChange W K)).pointEquivDegreeOnePlace T))) = ((TauCeti.Isogeny.mulByIntIsogeny (Affine.baseChange W K) ⋯).divisorPullback ⋯) (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint ↑((toAffine (Affine.baseChange W K)).pointEquivDegreeOnePlace ((Multiplicative.toAdd (W.pointGaloisAction σ)) T)))

Pullback along [n] is Galois-equivariant on points: an F-automorphism σ of a separably closed field K in which n is invertible carries [n]^* (T) to [n]^* (σ T).

@[simp]

theorem WeierstrassCurve.divisorGaloisAction_weilPairingDivisor {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] [IsSepClosed K] (W : WeierstrassCurve F) [W.IsElliptic] (σ : Gal(K/F)) {n : ℤ} (hchar : ↑n ≠ 0) (T : (toAffine (Affine.baseChange W K)).Point) : (Multiplicative.toAdd (W.divisorGaloisAction σ)) (TauCeti.Isogeny.weilPairingDivisor (Affine.baseChange W K) ⋯ T) = TauCeti.Isogeny.weilPairingDivisor (Affine.baseChange W K) ⋯ ((Multiplicative.toAdd (W.pointGaloisAction σ)) T)

The divisor [n]^* (T) - [n]^* (O) is Galois-equivariant: an F-automorphism σ of a separably closed field K in which n is invertible carries it to [n]^* (σ T) - [n]^* (O).

@[simp]

theorem WeierstrassCurve.weilPairing_torsionGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] [IsSepClosed K] (W : WeierstrassCurve F) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) (σ : Gal(K/F)) (S T : ↥(Submodule.torsionBy ℤ (toAffine (Affine.baseChange W K)).Point ↑N)) : ((TauCeti.Isogeny.weilPairing (Affine.baseChange W K) N hN) ((Multiplicative.toAdd ((W.torsionGaloisAction ↑N) σ)) S)) ((Multiplicative.toAdd ((W.torsionGaloisAction ↑N) σ)) T) = Additive.ofMul ((restrictRootsOfUnity σ N) (Additive.toMul (((TauCeti.Isogeny.weilPairing (Affine.baseChange W K) N hN) S) T)))

The Weil pairing is Galois-equivariant (Silverman III.8.1(e)): for an F-automorphism σ of a separably closed field K in which N is invertible, e_N(σ S, σ T) = σ (e_N(S, T)).