The determinant of an endomorphism on torsion

Let W be an elliptic curve over a separably closed field F and N a positive integer invertible in F. Then E[N] is free of rank two over ZMod N, and the Weil pairing is an alternating, nondegenerate pairing on it. An endomorphism of E[N] scaling the Weil pairing by d therefore has determinant d. A separable isogeny φ : W → W scales the Weil pairing by its degree, so the determinant of its action on E[N] is deg φ modulo N: the finite-level form of Silverman III.8.6, for separable φ.

This is how degrees become determinants of matrices over ZMod N in the Weil-pairing proof of the Hasse bound: once a basis of E[ℓ] is chosen, LinearMap.toMatrix turns the action of the pencil r π - s of the Frobenius π, for s not divisible by the characteristic (so that r π - s is separable), into a 2 × 2 matrix whose determinant is the degree of r π - s, as TauCeti.Matrix.eq_quadratic_form_of_det_det_one_sub requires.

Main results

• TauCeti.Isogeny.det_eq_of_weilPairing_eq_smul: an endomorphism of E[N] scaling the Weil pairing by d has determinant d.
• TauCeti.Isogeny.Hom.det_torsionLinearMap_ofIsogeny: the determinant of the action of a separable isogeny on E[N] is its degree.
• TauCeti.Isogeny.Hom.det_torsionLinearMap: the same for a nonzero separable morphism.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.8.6.

theorem TauCeti.Isogeny.det_eq_of_weilPairing_eq_smul {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) {f : Module.End (ZMod N) ↥(AddSubgroup.torsionBy W.Point ↑N)} {d : ZMod N} (hf : ∀ (S T : ↥(AddSubgroup.torsionBy W.Point ↑N)), ((weilPairing W N hN) (f S)) (f T) = d • ((weilPairing W N hN) S) T) : LinearMap.det f = d

An endomorphism of E[N] scaling the Weil pairing by d has determinant d, over a separably closed field in which N is invertible.

theorem TauCeti.Isogeny.Hom.det_torsionLinearMap_ofIsogeny {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) (φ : Isogeny W W) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W.FunctionField] : LinearMap.det ((ofIsogeny φ).torsionLinearMap N) = ↑φ.degree

The determinant of the action of a separable isogeny on E[N] is its degree modulo N, over a separably closed field in which N is invertible (Silverman III.8.6).

theorem TauCeti.Isogeny.Hom.det_torsionLinearMap {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) {f : Hom W W} (h : f ≠ 0) [Algebra.IsSeparable (↥(toIsogeny h).fieldPullback.fieldRange) W.FunctionField] : LinearMap.det (f.torsionLinearMap N) = ↑f.degree

The determinant of a nonzero separable morphism on E[N] is its degree modulo N, over a separably closed field in which N is invertible.