The degree of `1 − π_q` is the number of rational points #

Over a finite field the isogeny 1 − π_q has degree the number of rational points of the curve. One inequality is pointCount_le_degree_oneSubFrobeniusIsogeny: the kernel is every rational point and the kernel is at most the degree. This file supplies the other.

An isogeny here has no map on points, so the count is made on embeddings of the function field. Write L for the pulled-back field. Two embeddings of K(W) over L agree on L, so they move the tautological point of 1 − π_q to the same place; that image is the difference of the generic point's image and its q-power image, so the two images of the generic point differ by a point fixed by the q-power map, which therefore comes from the base field. An embedding is determined by where it sends the generic point, so the resulting assignment of a rational point to an embedding is injective. The separable degree is the number of such embeddings, and 1 − π_q is separable, so the degree is at most the point count.

Main results #

TauCeti.Isogeny.card_emb_oneSubFrobeniusIsogeny_le_pointCount: the embeddings of K(W) over the pulled-back field are at most as many as the rational points.
TauCeti.Isogeny.degree_oneSubFrobeniusIsogeny_le_pointCount: hence deg (1 − π_q) is at most the point count.
TauCeti.Isogeny.degree_oneSubFrobeniusIsogeny_eq_pointCount: with the reverse bound, deg (1 − π_q) = #E(𝔽_q).
TauCeti.Isogeny.card_ker_oneSubFrobeniusIsogeny_eq_degree: equivalently, the kernel of 1 − π_q has deg (1 − π_q) points.

References #

J. Silverman, The Arithmetic of Elliptic Curves, III.4.10 and V.1.1.

Provenance #

The route is that of the AINTLIB HasseWeil project (Chris Birkbeck, Apache-2.0) at commit 513e83879e2f8cbc626eb9e04d660e92be16ccba, HasseWeil/Isogeny/VerschiebungFactorization.lean, declaration emb_le_card_kernel, which assembles the same count at the point level. The proof differs in what it rests on: there an isogeny carries its own map on points and the argument is placed over AlgebraicClosure K(E) explicitly, while here the kernel is the translation-fixing subgroup of the pulled-back field and the embeddings are Mathlib's Field.Emb, so the descent is WeierstrassCurve.Affine.Point.map_frobeniusAlgHom_eq_self_iff_mem_range_baseChange and the injectivity is WeierstrassCurve.Affine.map_genericPoint_injective.

source

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

Nat.card (Field.Emb (↥(oneSubFrobeniusIsogeny W).fieldPullback.fieldRange) W.FunctionField) ≤ WeierstrassCurve.pointCount W

There are at most as many embeddings of the function field over the pulled-back field as there are rational points. Each embedding is sent to the rational point by which it moves the generic point away from a fixed base embedding.

source

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

(oneSubFrobeniusIsogeny W).degree ≤ WeierstrassCurve.pointCount W

The degree of 1 − π_q is at most the number of rational points, the isogeny being separable, so that its degree is the number of embeddings counted above.

source

@[simp]