The kernel of [n] has n ² points

Isogeny.ker counts only the base field's points, so its order equals the degree exactly when the geometric kernel is rational and the isogeny is separable: an inseparable isogeny has strictly fewer geometric kernel points than its degree even over an algebraically closed field. Separability of [n] is n being invertible in the base. Rationality is the other hypothesis, and it is the one that decides how general the statement is.

So the count is proved once with rationality as a hypothesis, and a closure assumption enters only in a corollary. An algebraically closed base gives rationality outright — no extension of it carries new torsion — which is card_ker_mulByIntIsogeny_of_isAlgClosed below. Keeping the hypothesis explicit is what lets the count be read at a base where the torsion is rational for some other reason, without the argument being repeated.

The count is made on embeddings, as for 1 − π_q: an isogeny here has no map on points. Two embeddings of K(W) over the pulled-back field move the tautological point of [n], which is n times the generic point, to the same place, so the two images of the generic point differ by an n-torsion point — and rationality is exactly what puts that difference in the kernel. An embedding is determined by where it sends the generic point, so that assignment is injective into the kernel, and the separable degree is the number of embeddings.

The extension rationality is needed over is AlgebraicClosure W.FunctionField, because Field.Emb K L is L →ₐ[K] AlgebraicClosure K: the embeddings being counted land in the algebraic closure of the pulled-back field, so that is where the torsion difference lives.

Main results

• TauCeti.Isogeny.card_ker_mulByIntIsogeny_of_torsion_rational: #ker [n] = n ² whenever the geometric n-torsion is rational and n is invertible.
• TauCeti.Isogeny.card_ker_mulByIntIsogeny_of_isAlgClosed: the same over an algebraically closed field.
• WeierstrassCurve.Affine.natCard_torsionBy_of_torsion_rational: the count read on Mathlib's intrinsic torsion subgroup.
• TauCeti.Isogeny.card_ker_mulByPrimeIsogeny_of_torsion_rational: the same at a prime, as ℓ ² rather than (ℓ : ℤ).natAbs ^ 2.
• WeierstrassCurve.finite_torsionBy: finiteness of E[n] for nonzero n, read on W.toAffine.Point itself rather than on the trivial base change W⁄K.

The three steps of the argument sketched above — the torsion difference, its rationality, and the resulting bound on embeddings — are private; nothing outside this module uses them.

References

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

theorem TauCeti.Isogeny.card_ker_mulByIntIsogeny_of_torsion_rational {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} {hn : psiFunctionField W n ≠ 0} (hrat : ∀ (P : (WeierstrassCurve.toAffine (W.baseChange (AlgebraicClosure W.FunctionField))).Point), n • P = 0 → P ∈ Set.range ⇑(WeierstrassCurve.Affine.Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑n ≠ 0) : Nat.card ↥(mulByIntIsogeny W hn).ker = n.natAbs ^ 2

#ker [n] = n ² whenever the geometric n-torsion is rational, for n invertible.

Isogeny.ker counts the base field's points, so the count is the degree exactly when the kernel is rational and the isogeny separable. Both obstructions are hypotheses here: rationality is hrat, separability is hchar. An algebraically closed base supplies the first for free, which is card_ker_mulByIntIsogeny_of_isAlgClosed.

theorem TauCeti.Isogeny.card_ker_mulByIntIsogeny_of_isAlgClosed {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [IsAlgClosed F] {n : ℤ} {hn : psiFunctionField W n ≠ 0} (hchar : ↑n ≠ 0) : Nat.card ↥(mulByIntIsogeny W hn).ker = n.natAbs ^ 2

#ker [n] = n ² over an algebraically closed field, for n invertible there: no extension of an algebraically closed field carries new torsion, which is the rationality the count needs.

This is the form the separability of the division polynomials is counted against, so it is the one that cannot ask only for a separably closed base; card_ker_mulByIntIsogeny is that stronger statement, proved from this one.

theorem WeierstrassCurve.Affine.natCard_torsionBy_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 • P = 0 → P ∈ Set.range ⇑(Point.baseChange F (AlgebraicClosure W.FunctionField))) (hchar : ↑n ≠ 0) : Nat.card ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point n) = n.natAbs ^ 2

#E[n] = n ² when the geometric n-torsion is rational and n is invertible: the count of ker [n] read on Mathlib's intrinsic torsion subgroup.

theorem WeierstrassCurve.Affine.finite_torsionBy {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) : Finite ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point n)

The n-torsion of an elliptic curve is finite for every nonzero integer n.

theorem WeierstrassCurve.finite_torsionBy {K : Type u_1} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {n : ℤ} (hn : n ≠ 0) : Finite ↥(AddSubgroup.torsionBy W.toAffine.Point n)

The n-torsion read on W.toAffine.Point itself, rather than on the trivial base change W⁄K, is finite for nonzero n.

theorem TauCeti.Isogeny.card_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) : Nat.card ↥(mulByPrimeIsogeny W l).ker = l ^ 2

#E[ℓ] = ℓ ² whenever the geometric ℓ-torsion is rational, for a prime ℓ invertible in the base: the integer count read at n = ℓ, where natAbs is the identity.