Galois actions on elliptic-curve points

Let W be a Weierstrass curve over a field F, and K an extension of F. An F-automorphism of K acts on the coordinates of the points of W over K, through the transport WeierstrassCurve.Affine.Point.mapEquiv. This file packages that as the Galois action on points and, restricting to the subgroup killed by N : ℤ, as the action on N-torsion. Both actions are bundled as monoid homomorphisms into the additive automorphism group, viewed multiplicatively so composition has the usual action order.

For N ≠ 0 the torsion action is the input needed to state Galois equivariance of the Weil pairing. When F is finite and K is an algebraic extension of F, the #F-power Frobenius is an F-automorphism of K, so the same action also supplies the point-side representation used in the Hasse-bound argument.

Main definitions

• WeierstrassCurve.pointGaloisAction: the Galois action on points.
• WeierstrassCurve.torsionGaloisAction: its restriction to N-torsion.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8 and V.1.

noncomputable def WeierstrassCurve.pointGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] (W : WeierstrassCurve F) : (K ≃ₐ[F] K) →* Multiplicative (AddAut (W.baseChange K).toAffine.Point)

The Galois action on the points of an elliptic curve. An F-automorphism of K acts by applying it to both affine coordinates and fixes the point at infinity.

Equations

• W.pointGaloisAction = { toFun := fun (e : K ≃ₐ[F] K) => Multiplicative.ofAdd (WeierstrassCurve.Affine.Point.mapEquiv W e), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem WeierstrassCurve.pointGaloisAction_apply {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] (W : WeierstrassCurve F) (e : K ≃ₐ[F] K) (P : (W.baseChange K).toAffine.Point) : (Multiplicative.toAdd (W.pointGaloisAction e)) P = (Affine.Point.map ↑e) P

The Galois action of e on points is Mathlib's point map along e.

noncomputable def WeierstrassCurve.torsionGaloisAction {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] (W : WeierstrassCurve F) (N : ℤ) : (K ≃ₐ[F] K) →* Multiplicative (AddAut ↥(AddSubgroup.torsionBy (W.baseChange K).toAffine.Point N))

The Galois action on N-torsion. This is the restriction of pointGaloisAction to the subgroup killed by N.

Equations

• W.torsionGaloisAction N = { toFun := fun (e : K ≃ₐ[F] K) => Multiplicative.ofAdd ((WeierstrassCurve.Affine.Point.mapEquiv W e).torsionByCongr N), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem WeierstrassCurve.torsionGaloisAction_apply_coe {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] (W : WeierstrassCurve F) (N : ℤ) (e : K ≃ₐ[F] K) (P : ↥(AddSubgroup.torsionBy (W.baseChange K).toAffine.Point N)) : ↑((Multiplicative.toAdd ((W.torsionGaloisAction N) e)) P) = (Multiplicative.toAdd (W.pointGaloisAction e)) ↑P

The Galois action on N-torsion agrees with the Galois action on points.