The isogeny 1 − π

For an elliptic curve W over a finite field F, the difference of the identity and the Frobenius isogeny π in the endomorphism carrier Hom W W is nonzero — the two have different degrees, by TauCeti.Isogeny.frobeniusIsogeny_ne_id — and so is an isogeny W → W. Its kernel is the group of F-rational points, and its degree is the number of them; this file provides the isogeny itself.

Main definitions

• TauCeti.Isogeny.oneSubFrobeniusIsogeny: the isogeny 1 − π.

Main results

• TauCeti.Isogeny.id_ne_ofIsogeny_frobeniusIsogeny: π is not the identity in Hom W W.
• TauCeti.Isogeny.ofIsogeny_oneSubFrobeniusIsogeny: in Hom W W, the isogeny 1 − π is 1 − π.

References

• J. Silverman, The Arithmetic of Elliptic Curves, V.2.

@[simp]

theorem TauCeti.Isogeny.id_ne_ofIsogeny_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) : Hom.id W ≠ Hom.ofIsogeny (frobeniusIsogeny W)

π is not the identity of the endomorphism carrier, stated in the form simp normalises 1 - π = 0 to.

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

The isogeny 1 − π: the difference of the identity and the Frobenius isogeny.

Equations

• TauCeti.Isogeny.oneSubFrobeniusIsogeny W = TauCeti.Isogeny.Hom.toIsogeny ⋯

@[simp]

theorem TauCeti.Isogeny.ofIsogeny_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : Hom.ofIsogeny (oneSubFrobeniusIsogeny W) = 1 - Hom.ofIsogeny (frobeniusIsogeny W)

1 − π in the endomorphism carrier: the isogeny oneSubFrobeniusIsogeny is the difference of 1 and the Frobenius isogeny in Hom W W.