The trace of Frobenius over a separably closed extension

Let W be an elliptic curve over a finite field 𝔽_q and π its Frobenius over a separably closed extension K. This file proves that deg (id - π) over K is #E(𝔽_q), the point count of W over its own base, and hence that the degree of the Frobenius pencil r π - s is the quadratic form q r² - a_q r s + s² whose middle coefficient is the Frobenius trace a_q = q + 1 - #E(𝔽_q).

Main results

• TauCeti.Isogeny.Hom.degree_id_sub_ofIsogeny_baseChangeFrobenius_eq_pointCount: deg (id - π) = #E(𝔽_q) over a separably closed extension.
• TauCeti.Isogeny.Hom.degree_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_eq_frobeniusTrace: the degree of r π - s is the quadratic form q r² - a_q r s + s².

References

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

Provenance

The AINTLIB HasseWeil project (Chris Birkbeck, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a has the corresponding count for its own model of isogenies, oneSubFrobeniusIsogBaseChange_degree_eq_pointCount in HasseWeil/HasseBound/WeilPairing/Scaling/OneSubTransport.lean. Nothing is taken from the source: the statements here are about TauCeti's morphisms of elliptic curves and their degrees.

theorem TauCeti.Isogeny.Hom.degree_id_sub_ofIsogeny_baseChangeFrobenius_eq_pointCount {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [IsSepClosed K] : (id (WeierstrassCurve.toAffine (W.baseChange K)) - ofIsogeny (baseChangeFrobenius K W)).degree = WeierstrassCurve.pointCount W

deg (id - π) = #E(𝔽_q): over a separably closed extension of the finite base, the degree of id - π is the number of rational points of W, the point at infinity included. Here π is the base-changed Frobenius endomorphism of W⁄K; compare TauCeti.Isogeny.degree_oneSubFrobeniusIsogeny_eq_pointCount, the same count for 1 - π_q as an isogeny of W over 𝔽_q itself.

theorem TauCeti.Isogeny.Hom.degree_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_eq_frobeniusTrace {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [IsSepClosed K] [Algebra.IsAlgebraic F K] (r s : ℤ) (hs : ↑s ≠ 0) : ↑(r • ofIsogeny (baseChangeFrobenius K W) - s • id (WeierstrassCurve.toAffine (W.baseChange K))).degree = ↑(Nat.card F) * r ^ 2 - WeierstrassCurve.frobeniusTrace W * (r * s) + s ^ 2

The middle coefficient of the Frobenius pencil's degree form is the Frobenius trace. Over a separably closed algebraic extension, deg (r π - s) = q r² - a_q r s + s² whenever s is nonzero in the field. Compare degree_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id, which has q + 1 - deg (id - π) in place of a_q.