[n] carries E[n ²] onto E[n]

Multiplication by n sends an n ²-torsion point to an n-torsion point, and once n is invertible in the base field and the geometric n ²-torsion is rational that map is onto: every n-torsion point is n times an n ²-torsion point.

The argument is counting, not geometry. #E[m] = m ² for every invertible m, so #E[n ²] = n ⁴ and #E[n] = n ²; the kernel of [n] : E[n ²] → E[n] consists of n-torsion points, so it has at most n ² elements, which is exactly #E[n ²] / #E[n]. A homomorphism of finite groups whose kernel is that small is surjective.

Main results

• WeierstrassCurve.Affine.zsmulTorsionSqHom_surjective_of_torsion_rational: [n] : E[n ²] → E[n] is onto.
• WeierstrassCurve.Affine.exists_zsmul_eq_of_zsmul_eq_zero_of_torsion_rational: hence every n-torsion point is n • P for some P killed by n ².

References

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

Provenance

The counting argument is adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0) pinned at a302aeacd86053f9d5f991fbbf664e1cc1051d08, HasseWeil/HasseBound/WeilPairing/Pairing.lean, declarations mulByEllTorsionHom_surjective and exists_preimage_of_torsion: the same three steps — the two torsion orders, the kernel's injection into E[n], and AddMonoidHom.surjective_of_card_ker_le_div. The orders come from this repository's own card_ker_mulByIntIsogeny_of_torsion_rational rather than from that project's separable-kernel torsor, and the statement is on AddSubgroup.torsionBy rather than on a bespoke torsion subgroup.

def WeierstrassCurve.Affine.zsmulTorsionSqHom {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) (n : ℤ) : ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point (n ^ 2)) →+ ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point n)

[n] as a map E[n ²] → E[n]: an n ²-torsion point is carried to an n-torsion one, since n • (n • P) = n ² • P.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Affine.zsmulTorsionSqHom_apply {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) (n : ℤ) (P : ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point (n ^ 2))) : ↑((W.zsmulTorsionSqHom n) P) = n • ↑P

The restricted multiplication homomorphism sends P to n • P.

theorem WeierstrassCurve.Affine.zsmulTorsionSqHom_surjective_of_torsion_rational {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hrat : ∀ (P : (toAffine (W.baseChange (AlgebraicClosure W.FunctionField))).Point), n ^ 2 • P = 0 → P ∈ Set.range ⇑(Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑n ≠ 0) : Function.Surjective ⇑(W.zsmulTorsionSqHom n)

[n] carries E[n ²] onto E[n] when the geometric n ²-torsion is rational and n is invertible. The kernel is n-torsion, so it has at most n ² elements, and that is exactly #E[n ²] / #E[n].

theorem WeierstrassCurve.Affine.exists_zsmul_eq_of_zsmul_eq_zero_of_torsion_rational {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hrat : ∀ (P : (toAffine (W.baseChange (AlgebraicClosure W.FunctionField))).Point), n ^ 2 • P = 0 → P ∈ Set.range ⇑(Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑n ≠ 0) {T : (toAffine (W.baseChange F)).Point} (hT : n • T = 0) : ∃ (P : (toAffine (W.baseChange F)).Point), n • P = T ∧ n ^ 2 • P = 0

Every n-torsion point is n times an n ²-torsion point when the geometric n ²-torsion is rational and n is invertible: the consumer-facing reading of zsmulTorsionSqHom_surjective_of_torsion_rational.