The isogeny 1 − π is separable

Over a finite field, the Frobenius isogeny π pulls the invariant differential ω back to 0, so the isogeny 1 − π pulls it back to ω itself; by the differential criterion, 1 − π is separable (Silverman III.5.5). This is the step through which the number of rational points, the size of the kernel of 1 − π, becomes a degree.

Main results

• TauCeti.Isogeny.pullbackDifferential_oneSubFrobeniusIsogeny_invariantDifferential: (1 − π)^*ω = ω.
• TauCeti.Isogeny.isSeparable_oneSubFrobeniusIsogeny: 1 − π is separable.

Provenance

The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) also establishes the separability of 1 − π, in AdditionPullback/Frobenius.lean, for its own notion of isogeny, which carries a map on points. Here the isogeny is a coordinate pullback and separability is that of the function-field extension it induces, as everywhere in TauCeti.Isogeny; nothing is taken from the source.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.5.5, V.1.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_oneSubFrobeniusIsogeny_invariantDifferential {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (oneSubFrobeniusIsogeny W).pullbackDifferential W.invariantDifferential = W.invariantDifferential

1 − π pulls the invariant differential back to itself, since Frobenius kills it.

theorem TauCeti.Isogeny.isSeparable_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : Algebra.IsSeparable (↥(oneSubFrobeniusIsogeny W).fieldPullback.fieldRange) W.FunctionField

The isogeny 1 − π is separable.