The kernel of multiplication by n is the n-torsion

An isogeny in this development has no point map, so its kernel is the subgroup of points whose translation fixes the pulled-back field (Isogeny.ker). For [n] that subgroup is the one the classical statement names: the n-torsion of W over the base field.

[n] is an isogeny only where the division polynomial does not vanish, so the statement carries psiFunctionField W n ≠ 0 — the same hypothesis mulByIntIsogeny is built from, and not a restriction beyond it. On an elliptic curve it holds for every n ≠ 0, by psiFunctionField_ne_zero_of_Δ_ne_zero.

The bridge is the tautological point. A coordinate pullback is determined by it, that of [n] is n times the generic point, and translating by P moves the generic point to g + P. So the translation fixes [n] exactly when n • (g + P) = n • g, which is n • P = 0.

Only the base field's points appear, as everywhere in Isogeny.ker: this is the rational n-torsion, not the geometric one, and the two differ unless the base field carries the whole kernel.

Main results

• TauCeti.Isogeny.mem_ker_mulByIntIsogeny_iff: P ∈ ker [n] ↔ n • P = 0, for an n whose division polynomial does not vanish, and TauCeti.Isogeny.mem_ker_mulByIntIsogenyOfNeZero_iff, the same at the n ≠ 0 the elliptic case discharges it from.
• TauCeti.Isogeny.ker_mulByIntIsogeny_eq_torsionBy: the same fact as an equality of subgroups, ker [n] = A[n] in Mathlib's intrinsic AddSubgroup.torsionBy form — the bridge a consumer of the torsion API needs.

Main definitions

• TauCeti.Isogeny.kerZModModule: the ZMod n-module structure the equality of subgroups transports onto ker [n]. It is a global instance, so typeclass synthesis supplies it and a consumer writing Module.finrank (ZMod n) (mulByIntIsogenyOfNeZero W hn).ker never names it.

References

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

theorem TauCeti.Isogeny.mem_ker_mulByIntIsogeny_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) {P : (WeierstrassCurve.toAffine (W.baseChange F)).Point} : P ∈ (mulByIntIsogeny W hn).ker ↔ n • P = 0

A point is in the kernel of [n] exactly when it is n-torsion, for an n whose division polynomial does not vanish — the hypothesis mulByIntIsogeny itself carries.

theorem TauCeti.Isogeny.mem_ker_mulByIntIsogenyOfNeZero_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) {P : (WeierstrassCurve.toAffine (W.baseChange F)).Point} : P ∈ (mulByIntIsogenyOfNeZero W hn).ker ↔ n • P = 0

A point is in the kernel of [n] exactly when it is n-torsion, with the non-vanishing hypothesis discharged from n ≠ 0 as in mulByIntIsogenyOfNeZero.

theorem TauCeti.Isogeny.ker_mulByIntIsogeny_eq_torsionBy {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).ker = AddSubgroup.torsionBy (WeierstrassCurve.toAffine (W.baseChange F)).Point n

The kernel of [n] is the n-torsion subgroup in Mathlib's intrinsic form A[n]. This is the bridge a consumer of the torsion API needs in order to transport results about the isogeny kernel to AddSubgroup.torsionBy. No primality is involved: it is mem_ker_mulByIntIsogeny_iff read as an equality of subgroups.

@[instance_reducible]

noncomputable instance TauCeti.Isogeny.kerZModModule {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℕ} (hn : ↑n ≠ 0) : Module (ZMod n) ↥(mulByIntIsogenyOfNeZero W hn).ker

The ZMod n-module structure on ker [n], transported from Mathlib's n-torsion module structure along ker_mulByIntIsogeny_eq_torsionBy. It is a global instance, so typeclass synthesis supplies it and a consumer writing Module.finrank (ZMod n) (mulByIntIsogenyOfNeZero W hn).ker never names it. Nothing about n beyond its not vanishing enters, so it is built here rather than at any specialization.

Equations

• TauCeti.Isogeny.kerZModModule W hn = ⋯ ▸ AddSubgroup.torsionBy.zmodModule