The ℓ-torsion is a two-dimensional ZMod ℓ-vector space

For a prime ℓ invertible in the base field, ker [ℓ] is free of rank two over ZMod ℓ as soon as the geometric ℓ-torsion is rational. Every point of the kernel is killed by ℓ, which makes it a ZMod ℓ-module, and ZMod ℓ is a field, so the kernel is a vector space whose cardinality ℓ ² reads off its dimension.

Beyond ℓ being invertible, rationality is the only thing the base field is asked for, so the statements take the two together, and a closure assumption enters only where the rationality is discharged.

Rank two is what lets an endomorphism act on the torsion as a 2 × 2 matrix over ZMod ℓ, which is the form the degree and the trace are read off in.

Main results

• TauCeti.Isogeny.finrank_ker_mulByPrimeIsogeny_of_torsion_rational: it has dimension two.
• TauCeti.Isogeny.nonempty_linearEquiv_ker_mulByPrimeIsogeny_of_torsion_rational: hence E[ℓ] ≅ (ZMod ℓ) ².

References

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

theorem TauCeti.Isogeny.finrank_ker_mulByPrimeIsogeny_of_torsion_rational {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {l : ℕ} [hl : Fact (Nat.Prime l)] (hrat : ∀ (P : (WeierstrassCurve.toAffine (W.baseChange (AlgebraicClosure W.FunctionField))).Point), ↑l • P = 0 → P ∈ Set.range ⇑(WeierstrassCurve.Affine.Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑l ≠ 0) : Module.finrank (ZMod l) ↥(mulByPrimeIsogeny W l).ker = 2

E[ℓ] is two-dimensional over ZMod ℓ for ℓ invertible in the base field whenever the geometric ℓ-torsion is rational.

theorem TauCeti.Isogeny.nonempty_linearEquiv_ker_mulByPrimeIsogeny_of_torsion_rational {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {l : ℕ} [hl : Fact (Nat.Prime l)] (hrat : ∀ (P : (WeierstrassCurve.toAffine (W.baseChange (AlgebraicClosure W.FunctionField))).Point), ↑l • P = 0 → P ∈ Set.range ⇑(WeierstrassCurve.Affine.Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑l ≠ 0) : Nonempty (↥(mulByPrimeIsogeny W l).ker ≃ₗ[ZMod l] Fin 2 → ZMod l)

E[ℓ] ≅ (ZMod ℓ)² for ℓ invertible in the base field whenever the geometric ℓ-torsion is rational: the ℓ-torsion is free of rank two.