The Frobenius isogeny kills the differentials

Over a finite field, the Frobenius isogeny of a Weierstrass curve pulls every differential of the function field back to zero. This is the differential-level form of its inseparability: the invariant differential in particular is pulled back to 0. The base-changed Frobenius over any field extension also kills the invariant differential.

Main results

• TauCeti.Isogeny.pullbackDifferential_frobeniusIsogeny: π^* is the zero map on differentials.
• TauCeti.Isogeny.pullbackDifferential_baseChangeFrobenius_invariantDifferential: the base-changed Frobenius kills the invariant differential over any field extension.

Provenance

The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) has the corresponding statements for the invariant differential only, omegaPullbackCoeff_frobenius and frobenius_pullbackKaehler_invariantDifferential in BridgeFrobenius.lean; the first statement here is for every differential of the function field.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.4.2, III.5.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : (frobeniusIsogeny W).pullbackDifferential = 0

The Frobenius isogeny pulls every differential back to zero.

@[simp]

theorem TauCeti.Isogeny.pullbackDifferential_baseChangeFrobenius_invariantDifferential {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) {K : Type u_2} [Field K] [Algebra F K] : (baseChangeFrobenius K W).pullbackDifferential (WeierstrassCurve.toAffine (W.baseChange K)).invariantDifferential = 0

The base-changed Frobenius kills the invariant differential, over any field extension.