Separability of multiplication by n

Whether [n] is separable is decided by its differential, and [n] = n • id computes that: the pullback of the invariant differential along [n] is n • ω, which vanishes exactly when n does in the base field. In characteristic zero, and in characteristic p for p ∤ n, [n] is therefore separable, and then nothing is inseparable in it, so its separable degree is its whole degree n ².

Main results

• TauCeti.Isogeny.isSeparable_mulByIntIsogeny_iff: [n] is separable exactly when n is nonzero in the base field.
• TauCeti.Isogeny.separableDegree_mulByIntIsogeny: in that case its separable degree is n ².

References

• [J. Silverman, The Arithmetic of Elliptic Curves][silverman2009], III.5.4 and III.6.

theorem TauCeti.Isogeny.pullbackDifferential_mulByIntIsogeny_invariantDifferential {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).pullbackDifferential W.invariantDifferential = n • W.invariantDifferential

[n] scales the invariant differential by n: the pullback of ω along [n] is n • ω. This is the differential computation the separability criterion for [n] rests on.

@[simp]

theorem TauCeti.Isogeny.isSeparable_mulByIntIsogeny_iff {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : Algebra.IsSeparable (↥(mulByIntIsogeny W hn).fieldPullback.fieldRange) W.FunctionField ↔ ↑n ≠ 0

[n] is separable exactly when n is nonzero in the base field (Silverman III.5.4).

theorem TauCeti.Isogeny.separableDegree_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} {hn : psiFunctionField W n ≠ 0} (hchar : ↑n ≠ 0) : (mulByIntIsogeny W hn).separableDegree = n.natAbs ^ 2

A separable [n] has separable degree n ², its degree, since nothing is inseparable.