The finite-level torsion structure of an elliptic curve

Over a separably closed field, the N-torsion of an elliptic curve is a product of two cyclic groups of order N, provided that N is invertible in the field. This identifies the finite torsion available for studying isogenies and the Weil pairing. Upgrading this along the canonical ZMod N-module structure on E[N], the N-torsion has a basis of two points over ZMod N.

Main definitions

• TauCeti.Isogeny.pointTorsionModule: the canonical ZMod N-module structure on N-torsion points.

Main results

• WeierstrassCurve.torsion_addEquiv_prod: E[N] ≃+ ZMod N × ZMod N.
• WeierstrassCurve.nonempty_basis_torsionBy: E[N] has a basis of two points over ZMod N.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(b).

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.pointTorsionModule {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (N : ℕ) : Module (ZMod N) ↥(AddSubgroup.torsionBy W.Point ↑N)

The canonical ZMod N-module structure on the N-torsion points of a Weierstrass curve. Mathlib supplies it only as the opt-in definition AddSubgroup.torsionBy.zmodModule; it is a global instance here, restricted to curve points, so that consumers of the torsion (bases, LinearMap.toMatrix, Module.finrank, and the action Hom.torsionLinearMap of morphisms) synthesize it.

Equations

• TauCeti.Isogeny.pointTorsionModule W N = AddSubgroup.torsionBy.zmodModule

theorem WeierstrassCurve.torsion_addEquiv_prod {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : Nonempty (↥(AddSubgroup.torsionBy W.toAffine.Point ↑N) ≃+ ZMod N × ZMod N)

E[N] ≃+ (ℤ/N)² over a separably closed field in which N is invertible.

The equivalence is noncanonical, so the result asserts its existence.

theorem WeierstrassCurve.nonempty_basis_torsionBy {K : Type u_1} [Field K] [IsSepClosed K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (N : ℕ) [NeZero N] (hN : ↑N ≠ 0) : Nonempty (Module.Basis (Fin 2) (ZMod N) ↥(AddSubgroup.torsionBy W.toAffine.Point ↑N))

E[N] has a basis of two points over ZMod N, over a separably closed field in which N is invertible. It identifies E[N] with the rank-two free module ZMod N × ZMod N, so that the action of an endomorphism on E[N] is a 2 × 2 matrix over ZMod N and has a determinant and trace. The basis is noncanonical, so the result asserts its existence.