Torsion over a separably closed field

Rationality of geometric torsion over a separably closed field is the hypothesis the counts of MulByInt/ take of the base field, so each of them holds here and the algebraically closed hypothesis they carried weakens to a separably closed one. The rationality theorem itself lives with the division-polynomial torsion theory in DivisionPolynomial.Torsion.IsSepClosed.

Main results

• TauCeti.Isogeny.card_ker_mulByIntIsogeny and WeierstrassCurve.Affine.natCard_torsionBy: #E[n] = n ², in the kernel and the torsion-subgroup forms.
• WeierstrassCurve.natCard_torsionBy: the same count read on W.toAffine.Point itself, rather than on the trivial base change W⁄K.
• TauCeti.Isogeny.card_ker_mulByPrimeIsogeny, TauCeti.Isogeny.finrank_ker_mulByPrimeIsogeny and TauCeti.Isogeny.nonempty_linearEquiv_ker_mulByPrimeIsogeny: E[ℓ] ≅ (ZMod ℓ) ² at a prime.
• WeierstrassCurve.Affine.zsmulTorsionSqHom_surjective and WeierstrassCurve.Affine.exists_zsmul_eq_of_zsmul_eq_zero: [n] carries E[n ²] onto E[n].
• WeierstrassCurve.Affine.exists_point_zsmul_eq_of_zsmul_eq_zero and WeierstrassCurve.Affine.natCard_setOf_zsmul_eq_zero: the same two facts on the points of W itself rather than of W⁄F.
• WeierstrassCurve.Affine.infinite_point: the points of W are infinitely many, the torsion alone being unbounded.

References

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

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

#ker [n] = n ² over a separably closed field, for n invertible there: the geometric n-torsion is then rational, which is the only thing the count asks of the base field.

theorem TauCeti.Isogeny.card_ker_mulByPrimeIsogeny {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {l : ℕ} [hl : Fact (Nat.Prime l)] (hchar : ↑l ≠ 0) : Nat.card ↥(mulByPrimeIsogeny W l).ker = l ^ 2

#E[ℓ] = ℓ ², for a prime ℓ invertible in a separably closed base field.

@[simp]

theorem TauCeti.Isogeny.finrank_ker_mulByPrimeIsogeny {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {l : ℕ} [hl : Fact (Nat.Prime l)] (hchar : ↑l ≠ 0) : Module.finrank (ZMod l) ↥(mulByPrimeIsogeny W l).ker = 2

E[ℓ] is two-dimensional over ZMod ℓ for a prime ℓ invertible in a separably closed base field, where the geometric ℓ-torsion is rational.

theorem TauCeti.Isogeny.nonempty_linearEquiv_ker_mulByPrimeIsogeny {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {l : ℕ} [hl : Fact (Nat.Prime l)] (hchar : ↑l ≠ 0) : Nonempty (↥(mulByPrimeIsogeny W l).ker ≃ₗ[ZMod l] Fin 2 → ZMod l)

E[ℓ] ≅ (ZMod ℓ)² for a prime ℓ invertible in a separably closed base field.

theorem WeierstrassCurve.Affine.natCard_torsionBy {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hchar : ↑n ≠ 0) : Nat.card ↥(AddSubgroup.torsionBy (toAffine (W.baseChange F)).Point n) = n.natAbs ^ 2

#E[n] = n ² over a separably closed field in which n is invertible, read on Mathlib's intrinsic torsion subgroup.

theorem WeierstrassCurve.Affine.zsmulTorsionSqHom_surjective {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hchar : ↑n ≠ 0) : Function.Surjective ⇑(W.zsmulTorsionSqHom n)

[n] carries E[n ²] onto E[n] over a separably closed field in which n is invertible.

theorem WeierstrassCurve.Affine.exists_zsmul_eq_of_zsmul_eq_zero {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (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, over a separably closed field in which n is invertible.

theorem WeierstrassCurve.Affine.exists_point_zsmul_eq_of_zsmul_eq_zero {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hchar : ↑n ≠ 0) {T : W.Point} (hT : n • T = 0) : ∃ (R : W.Point), n • R = T

Every n-torsion point of W is n times a point of W, over a separably closed field in which n is invertible.

theorem WeierstrassCurve.Affine.natCard_setOf_zsmul_eq_zero {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hchar : ↑n ≠ 0) : Nat.card ↑{R : W.Point | n • R = 0} = n.natAbs ^ 2

#E[n] = n ² over a separably closed field in which n is invertible, counted on the points of W themselves.

instance WeierstrassCurve.Affine.infinite_point {F : Type u_1} [Field F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : Infinite W.Point

An elliptic curve has infinitely many points over a separably closed field: for every prime ℓ other than the characteristic, its ℓ-torsion alone has ℓ ² points.

theorem WeierstrassCurve.natCard_torsionBy {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {n : ℤ} (hn : ↑n ≠ 0) : Nat.card ↥(AddSubgroup.torsionBy W.toAffine.Point n) = n.natAbs ^ 2

The n-torsion read on W.toAffine.Point itself, rather than on the trivial base change W⁄K, has order n.natAbs ^ 2 when n is invertible in K.