Multiplication by n is surjective over a separably closed field

Let W be an elliptic curve over a separably closed field F, and n an integer invertible in F. Then every point of W is divisible by n: the map P ↦ n • P on W(F) is surjective (Silverman III.4.2(a) with III.5.4). This is the right-exactness of the sequence 0 → E[n] → E(Kˢ) → E(Kˢ) → 0 on which the Galois-cohomological n-descent rests.

The proof goes through the isogeny [n]. It is separable because n is invertible (TauCeti.Isogeny.isSeparable_mulByIntIsogeny_iff), a separable isogeny is surjective on points over a separably closed field (TauCeti.Isogeny.toPointHom_surjective), and its action on points is multiplication by n (TauCeti.Isogeny.ofIsogeny_mulByIntIsogeny).

The invertibility hypothesis cannot be dropped. Over a separably closed field of characteristic p that is not perfect, the fibres of the inseparable isogeny [p] live in a purely inseparable extension, so [p] need not be surjective on points.

Main results

• WeierstrassCurve.Affine.zsmul_surjective: P ↦ n • P is surjective for n : ℤ invertible in the base field.
• WeierstrassCurve.Affine.nsmul_surjective: the same for n : ℕ.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.2(a) and III.5.4.

theorem WeierstrassCurve.Affine.zsmul_surjective {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : ↑n ≠ 0) : Function.Surjective fun (P : W.Point) => n • P

Multiplication by n is surjective on the points of an elliptic curve over a separably closed field, for n invertible in the field (Silverman III.4.2(a), III.5.4).

theorem WeierstrassCurve.Affine.nsmul_surjective {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℕ} (hn : ↑n ≠ 0) : Function.Surjective fun (P : W.Point) => n • P

Multiplication by a natural number n is surjective on the points of an elliptic curve over a separably closed field, for n invertible in the field.