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 ².
• TauCeti.Isogeny.dvd_inseparableDegree_mulByIntIsogeny: when n vanishes in the base field, the characteristic divides the inseparable degree of [n].
• TauCeti.Isogeny.inseparableDegree_mulByIntIsogenyOfNeZero_pow: the inseparable degree of [n ^ k] is the k-th power of that of [n].

References

• J. Silverman, The Arithmetic of Elliptic Curves, 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.

theorem TauCeti.Isogeny.dvd_inseparableDegree_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (p : ℕ) [ExpChar F p] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (hchar : ↑n = 0) : p ∣ (mulByIntIsogeny W hn).inseparableDegree

The inseparable degree of [n] is divisible by the characteristic when n vanishes in the base field.

theorem TauCeti.Isogeny.inseparableDegree_mulByIntIsogenyOfNeZero_pow {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) (k : ℕ) : (mulByIntIsogenyOfNeZero W ⋯).inseparableDegree = (mulByIntIsogenyOfNeZero W hn).inseparableDegree ^ k

The inseparable degree of [n ^ k] is the k-th power of that of [n].