The dual of 1 − π_q

Over a finite field 𝔽_q the kernel of 1 − π_q is the set of all rational points, and its degree is their number #E(𝔽_q). So 1 − π_q satisfies the hypothesis #ker φ = deg φ of Isogeny/Dual/Basic.lean, and [#E(𝔽_q)] factors through it. The factor is the dual (1 − π_q)^, of degree #E(𝔽_q). The classical identities (1 − π_q)^ = 1 − π̂_q and π_q + π̂_q = [a_q] are not proved here.

Main results

• TauCeti.Isogeny.existsUnique_comp_oneSubFrobeniusIsogeny_eq_mulByIntIsogenyOfNeZero: there is a unique χ with χ ∘ (1 − π_q) = [#E(𝔽_q)].
• TauCeti.Isogeny.degree_eq_pointCount_of_comp_oneSubFrobeniusIsogeny_eq: any such χ has degree #E(𝔽_q).

References

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

theorem TauCeti.Isogeny.existsUnique_comp_oneSubFrobeniusIsogeny_eq_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : ∃! χ : Isogeny W W, χ.comp (oneSubFrobeniusIsogeny W) = mulByIntIsogenyOfNeZero W ⋯

[#E(𝔽_q)] factors through 1 − π_q, by a unique isogeny: the dual of 1 − π_q.

theorem TauCeti.Isogeny.degree_eq_pointCount_of_comp_oneSubFrobeniusIsogeny_eq {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {χ : Isogeny W W} (h : χ.comp (oneSubFrobeniusIsogeny W) = mulByIntIsogenyOfNeZero W ⋯) : χ.degree = WeierstrassCurve.pointCount W

The dual of 1 − π_q has degree #E(𝔽_q).