Every rational point lies in the kernel of 1 − π

Over a finite field the isogeny 1 − π_q kills every F-rational point, so its kernel is all of them. The reason is the one behind the classical count: π_q fixes the rational points, so (1 − π_q)(X + P) = (1 − π_q)(X) for rational P, and a function pulled back along 1 − π_q is unmoved by translating by P.

An isogeny here has no point map, so the argument is carried out on tautological points. A kernel element is a point whose translation fixes the pulled-back field; translation acts on a pullback by post-composition, and a pullback is fixed by such an endomorphism exactly when its tautological point is. The tautological point of 1 − π_q is g − π_q(g), and translation moves both terms by the same rational point, so their difference does not move at all.

Main results

• TauCeti.Isogeny.ker_oneSubFrobeniusIsogeny: the kernel of 1 − π_q is everything.
• TauCeti.Isogeny.card_ker_oneSubFrobeniusIsogeny: so its kernel has exactly as many elements as there are rational points.
• TauCeti.Isogeny.pointCount_le_degree_oneSubFrobeniusIsogeny: consequently deg (1 − π_q) bounds pointCount above.
• TauCeti.Isogeny.pointCount_dvd_degree_oneSubFrobeniusIsogeny: and, 1 − π_q being separable, pointCount divides deg (1 − π_q).

This is the lower half of deg (1 − π_q) = #E(𝔽_q). The upper half asks in addition that the kernel cut out the pulled-back field exactly, and is not proved here.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4, V.1.
• The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) states the two headline results in Hasse/PointFix.lean as kernel_eq_top_of_hom_eq_id_sub_frobenius and card_kernel_eq_pointCount_of_kernel_eq_top. Its isogenies carry a point map independent of the function-field pullback, and its Frobenius declares that map to be the identity, so there the first reduces to sub_self. The kernel here is defined from the pullback, so the proof is the tautological-point argument above instead.

@[simp]

theorem TauCeti.Isogeny.ker_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (oneSubFrobeniusIsogeny W).ker = ⊤

The kernel of 1 − π_q is every rational point.

theorem TauCeti.Isogeny.card_ker_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : Nat.card ↥(oneSubFrobeniusIsogeny W).ker = Nat.card (WeierstrassCurve.toAffine (W.baseChange F)).Point

The rational points are exactly the kernel of 1 − π_q, as a cardinality.

theorem TauCeti.Isogeny.pointCount_le_degree_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : WeierstrassCurve.pointCount W ≤ (oneSubFrobeniusIsogeny W).degree

The degree of 1 − π_q bounds the point count above. This is the lower half of deg (1 − π_q) = #E(𝔽_q); the upper half asks in addition that the kernel cut out the pulled-back field exactly, and is not proved here.

theorem TauCeti.Isogeny.pointCount_dvd_degree_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : WeierstrassCurve.pointCount W ∣ (oneSubFrobeniusIsogeny W).degree

The point count divides the degree of 1 − π_q. The kernel order always divides the separable degree, and 1 − π_q is separable, so the bound above is a divisibility. Equality is the upper half, which is not proved here.