noncomputable def Isogeny.restrictTorsion {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ℤ) : ↥(E.torsionSubgroup n) →+ ↥(E.torsionSubgroup n)

The restriction of an endomorphism α : E → E to the n-torsion subgroup, viewed as an additive group homomorphism E[n] →+ E[n].

@[simp]

theorem Isogeny.restrictTorsion_coe {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ℤ) (P : ↥(E.torsionSubgroup n)) : ↑((α.restrictTorsion n) P) = α.toAddMonoidHom ↑P

The restriction to torsion commutes with the inclusion E[n] ↪ E: the underlying point of α.restrictTorsion n P is just α(P).

noncomputable def torsionMatrixFromEndomorphism (n : ℕ) (f : ZMod n × ZMod n →+ ZMod n × ZMod n) : Matrix (Fin 2) (Fin 2) (ZMod n)

Given an additive endomorphism f of (ZMod n)², extract its matrix Mat₂(ZMod n) with respect to the standard basis (1,0), (0,1).

noncomputable def Isogeny.torsionMatrix {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ℕ) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) : Matrix (Fin 2) (Fin 2) (ZMod n)

The matrix of α acting on the n-torsion E[n], computed by conjugating the restriction with an isomorphism e : E[n] ≃+ (ZMod n)² to standard basis.

noncomputable def Isogeny.torsionTrace {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ℕ) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) : ZMod n

The trace mod n of α on the n-torsion: the trace of α.torsionMatrix n e.

noncomputable def Isogeny.torsionDet {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α : Isogeny E E) (n : ℕ) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) : ZMod n

The determinant mod n of α on the n-torsion: the determinant of α.torsionMatrix n e.

theorem Matrix.cayleyHamilton_fin_two (n : ℕ) (M : Matrix (Fin 2) (Fin 2) (ZMod n)) : M * M - M.trace • M + M.det • 1 = 0

The Cayley–Hamilton theorem for 2 × 2 matrices over ZMod n: every such matrix M satisfies M² - tr(M) • M + det(M) • I = 0.

theorem Isogeny.charPoly_torsionMatrix {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) (n : ℕ) (hn_pos : 0 < n) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) : have M := α.torsionMatrix n e; have t := ↑(α.traceAux oneMinusAlpha h_oma); have d := ↑α.degree; M * M - t • M + d • 1 = 0

The torsion matrix of α satisfies the characteristic equation M² - t • M + d • I = 0, where t is the algebraic trace (from α.traceAux) reduced mod n and d is the degree of α mod n.

theorem Matrix.constraint_from_two_char_polys (n : ℕ) (M : Matrix (Fin 2) (Fin 2) (ZMod n)) (t d : ZMod n) (hrestr : M * M - t • M + d • 1 = 0) (hCH : M * M - M.trace • M + M.det • 1 = 0) : (M.trace - t) • M + (d - M.det) • 1 = 0

If M satisfies two characteristic equations M² - t•M + d•I = 0 and M² - tr(M)•M + det(M)•I = 0 (Cayley–Hamilton), then their difference yields (tr M - t)•M + (d - det M)•I = 0.

theorem Isogeny.constraint_resolution {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) (n : ℕ) (hn_pos : 0 < n) (hn_cop : n.Coprime (ringChar F)) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) (hconstraint : have M := α.torsionMatrix n e; have t := ↑(α.traceAux oneMinusAlpha h_oma); have d := ↑α.degree; (M.trace - t) • M + (d - M.det) • 1 = 0) : ↑(α.traceAux oneMinusAlpha h_oma) = (α.torsionMatrix n e).trace ∧ ↑α.degree = (α.torsionMatrix n e).det

From the relation (tr M - t)•M + (d - det M)•I = 0 on the torsion matrix, deduce that the algebraic trace equals tr M and the degree equals det M modulo n (requires n coprime to the characteristic).

theorem Isogeny.torsionMatrix_trace_det_resolution {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) (n : ℕ) (hn_pos : 0 < n) (hn_cop : n.Coprime (ringChar F)) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) (hrestr : have M := α.torsionMatrix n e; have t := ↑(α.traceAux oneMinusAlpha h_oma); have d := ↑α.degree; M * M - t • M + d • 1 = 0) (hCH : have M := α.torsionMatrix n e; M * M - M.trace • M + M.det • 1 = 0) : ↑(α.traceAux oneMinusAlpha h_oma) = (α.torsionMatrix n e).trace ∧ ↑α.degree = (α.torsionMatrix n e).det

Combining the characteristic equation from α's algebraic data with Cayley–Hamilton on the torsion matrix yields that the algebraic trace and degree of α agree mod n with the trace and determinant of α.torsionMatrix n e.

theorem Isogeny.trace_mod_n_eq {F : Type u} [Field F] [DecidableEq F] {E : WeierstrassCurve.Affine F} (α oneMinusAlpha : Isogeny E E) (h_oma : oneMinusAlpha.toAddMonoidHom = E.multiplicationByN 1 - α.toAddMonoidHom) (n : ℕ) (hn_pos : 0 < n) (hn_cop : n.Coprime (ringChar F)) (e : ↥(E.torsionSubgroup ↑n) ≃+ ZMod n × ZMod n) : ↑(α.traceAux oneMinusAlpha h_oma) = α.torsionTrace n e

The algebraic trace of an endomorphism α, reduced mod n, equals the trace of α acting on the n-torsion: tr(α) ≡ tr(α | E[n]) (mod n) when n is coprime to char F. This is the key compatibility used in the Tate module trace construction.