The action of an elliptic-curve morphism on torsion

A morphism of elliptic curves sends N-torsion points to N-torsion points. This file packages that action as a ZMod N-linear map, the restriction TauCeti.torsionByMap of the morphism's point map. The construction is functorial in the morphism: it respects zero, identities, addition, negation, subtraction, integer multiples and composition.

The finite-level action is the bridge from the intrinsic endomorphism ring to matrices. Whenever E[N] is free over ZMod N (for instance of rank two, when F is separably closed and N is invertible in F), LinearMap.toMatrix turns each value of Hom.torsionRepresentation into a matrix after a basis is chosen; this is the matrix representation used in the Weil-pairing proof of the Hasse bound. There, Hom.torsionLinearMap_apply supplies the point-map hypotheses of TauCeti.Isogeny.weilPairing_eq_degree_nsmul_weilPairing, which says that a separable isogeny scales the Weil pairing by its degree.

Main definitions

• TauCeti.Isogeny.Hom.torsionLinearMap: the ZMod N-linear action of a morphism on N-torsion.
• TauCeti.Isogeny.Hom.torsionRepresentation: the resulting ring representation of End(E).

Main results

• TauCeti.Isogeny.Hom.torsionLinearMap_comp: the torsion action is functorial.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.4 and III.8.

noncomputable def TauCeti.Isogeny.Hom.torsionLinearMap {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (N : ℕ) : ↥(AddSubgroup.torsionBy W₁.Point ↑N) →ₗ[ZMod N] ↥(AddSubgroup.torsionBy W₂.Point ↑N)

The action of a morphism on N-torsion, as a ZMod N-linear map.

The underlying additive map is TauCeti.torsionByMap applied to Hom.pointMapHom: the point map restricted to the torsion submodules, which lands in the target torsion because it is additive.

Equations

• f.torsionLinearMap N = AddMonoidHom.toZModLinearMap N (TauCeti.torsionByMap (↑N) f.pointMapHom.toIntLinearMap).toAddMonoidHom

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_apply {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (N : ℕ) (P : ↥(AddSubgroup.torsionBy W₁.Point ↑N)) : ↑((f.torsionLinearMap N) P) = f.pointMap ↑P

The torsion action is the morphism's point map on underlying points.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_zero {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (N : ℕ) : torsionLinearMap 0 N = 0

The zero morphism acts as the zero map on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_id {F : Type u_1} [Field F] [DecidableEq F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] (N : ℕ) : (id W₁).torsionLinearMap N = LinearMap.id

The identity morphism acts as the identity map on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_add {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f g : Hom W₁ W₂) (N : ℕ) : (f + g).torsionLinearMap N = f.torsionLinearMap N + g.torsionLinearMap N

The torsion action is additive in the morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_neg {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (N : ℕ) : (-f).torsionLinearMap N = -f.torsionLinearMap N

Negating a morphism negates its action on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_sub {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f g : Hom W₁ W₂) (N : ℕ) : (f - g).torsionLinearMap N = f.torsionLinearMap N - g.torsionLinearMap N

Subtraction of morphisms becomes subtraction of their actions on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_zsmul {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (N : ℕ) (n : ℤ) : (n • f).torsionLinearMap N = n • f.torsionLinearMap N

Integer multiples of a morphism act by the same integer multiple on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_nsmul {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (f : Hom W₁ W₂) (N n : ℕ) : (n • f).torsionLinearMap N = n • f.torsionLinearMap N

Natural multiples of a morphism act by the same natural multiple on torsion.

@[simp]

theorem TauCeti.Isogeny.Hom.torsionLinearMap_comp {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] [WeierstrassCurve.IsElliptic W₃] (g : Hom W₂ W₃) (f : Hom W₁ W₂) (N : ℕ) : (g.comp f).torsionLinearMap N = g.torsionLinearMap N ∘ₗ f.torsionLinearMap N

The torsion action is functorial: the action of a composite is the composite of the actions.

noncomputable def TauCeti.Isogeny.Hom.torsionRepresentation {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) : Hom W W →+* Module.End (ZMod N) ↥(AddSubgroup.torsionBy W.Point ↑N)

The action of the endomorphism ring on N-torsion. This packages additivity and functoriality of torsionLinearMap as a ring homomorphism, ready to be written as matrices after choosing a basis of the torsion module whenever it is free.

Equations

• TauCeti.Isogeny.Hom.torsionRepresentation W N = { toFun := fun (f : TauCeti.Isogeny.Hom W W) => f.torsionLinearMap N, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.Isogeny.Hom.torsionRepresentation_apply {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (N : ℕ) (f : Hom W W) : (torsionRepresentation W N) f = f.torsionLinearMap N

The torsion representation sends an endomorphism to its torsion linear map.