The dual of the Frobenius isogeny #

Let W be an elliptic curve over a finite field F with q elements and π = π_q : W → W its Frobenius isogeny, of degree q. This file constructs the dual isogeny π̂ : W → W of π, the unique isogeny with π̂ ∘ π = [q] (Silverman III.6.1), and proves its first properties: π ∘ π̂ = [q] as well, deg π̂ = q, and composition with π̂ is additive in the inner morphism. Classically π̂ is the q-power Verschiebung of W.

The Frobenius isogeny is purely inseparable, so this is the inseparable case of the dual-isogeny construction, the one not covered by TauCeti.Isogeny.dual, which takes a separable isogeny over a separably closed field. The construction goes through the factorisation theorem on function fields: [q] factors through π because [q]^* F(W) lies in the field π^* F(W) of q-th powers (Silverman II.2.12).

The Frobenius identities π ∘ π̂ = [q], proved here, and π + π̂ = [a_q], with a_q the trace of Frobenius, are the relations from which the degree form on the endomorphisms ℤ[π] of W, and with it the Hasse bound, are computed. The second is not proved here.

Main definitions #

TauCeti.Isogeny.dualFrobeniusIsogeny: the dual π̂ of the Frobenius isogeny.

Main results #

TauCeti.Isogeny.fieldRange_mulByIntIsogenyOfNeZero_card_le_fieldRange_frobeniusIsogeny: [q]^* F(W) ≤ π^* F(W).
TauCeti.Isogeny.existsUnique_comp_frobeniusIsogeny_eq_mulByIntIsogenyOfNeZero: [q] factors through π by a unique isogeny.
TauCeti.Isogeny.dualFrobeniusIsogeny_comp_frobeniusIsogeny and TauCeti.Isogeny.eq_dualFrobeniusIsogeny_iff_comp_eq: π̂ ∘ π = [q], and this characterises π̂.
TauCeti.Isogeny.frobeniusIsogeny_comp_dualFrobeniusIsogeny: π ∘ π̂ = [q].
TauCeti.Isogeny.degree_dualFrobeniusIsogeny: deg π̂ = q.
TauCeti.Isogeny.ofIsogeny_dualFrobeniusIsogeny_comp_ofIsogeny_frobeniusIsogeny and TauCeti.Isogeny.ofIsogeny_frobeniusIsogeny_comp_ofIsogeny_dualFrobeniusIsogeny: both composites are q • 1 in the additive group of endomorphisms.
TauCeti.Isogeny.pointMap_dualFrobeniusIsogeny_pointMap_frobeniusIsogeny and TauCeti.Isogeny.pointMap_frobeniusIsogeny_pointMap_dualFrobeniusIsogeny: on points, π̂ (π P) = q • P and π (π̂ P) = q • P.
TauCeti.Isogeny.Hom.dualFrobenius_comp_add, TauCeti.Isogeny.Hom.dualFrobenius_comp_sub and TauCeti.Isogeny.Hom.dualFrobenius_comp_zsmul: composition with π̂ is ℤ-linear in the inner morphism.

References #

J. Silverman, The Arithmetic of Elliptic Curves, II.2.11, II.2.12, III.6.1 and V.2.

source

theorem TauCeti.Isogeny.fieldRange_mulByIntIsogenyOfNeZero_card_le_fieldRange_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] :

(mulByIntIsogenyOfNeZero W ⋯).fieldPullback.fieldRange ≤ (frobeniusIsogeny W).fieldPullback.fieldRange

The function field pulled back by [q] lies inside the one pulled back by Frobenius: [q]^* F(W) ≤ π^* F(W), the latter being the field of q-th powers.

source

theorem TauCeti.Isogeny.existsUnique_comp_frobeniusIsogeny_eq_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] :

∃! χ : Isogeny W W, χ.comp (frobeniusIsogeny W) = mulByIntIsogenyOfNeZero W ⋯

[q] factors through the Frobenius isogeny by a unique isogeny: the dual of π_q (Silverman III.6.1).

source

noncomputable def TauCeti.Isogeny.dualFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] :

Isogeny W W

The dual of the Frobenius isogeny π̂ : W → W, the unique isogeny with π̂ ∘ π = [q] (Silverman III.6.1); classically, the q-power Verschiebung.

Equations