Degrees of the Frobenius pencil

Let W be an elliptic curve over a finite field F, and let π be its Frobenius over an extension K. The endomorphism r • π - s • id pulls the invariant differential back to -s • ω. Consequently it is nonzero and separable whenever s is nonzero in K.

Over a separably closed extension, the determinant of this pencil on N-torsion is its degree modulo N whenever N is invertible and s is nonzero in the field. If the extension is also algebraic, the degree is the integral quadratic form #F * r² - (#F + 1 - deg (id - π)) * r * s + s². This is the degree-form input to the Hasse bound.

Main results

• TauCeti.Isogeny.Hom.zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_ne_zero: the pencil is nonzero when s is nonzero in the field.
• TauCeti.Isogeny.Hom.isSeparable_toIsogeny_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_iff: a nonzero pencil is separable exactly when s is nonzero in the field.
• TauCeti.Isogeny.Hom.det_torsionLinearMap_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id: over a separably closed extension, the determinant on invertible torsion is the degree modulo N when s is nonzero in the field.
• TauCeti.Isogeny.Hom.degree_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id: the integral quadratic degree formula over a separably closed algebraic extension when s is nonzero in the field.

Provenance

The AINTLIB HasseWeil project (Chris Birkbeck, Apache 2.0, commit 513e83879e2f8cbc626eb9e04d660e92be16ccba) has conditional degree-form counterparts in DegreeQuadraticForm.lean (dual-isogeny witnesses) and WeilPairing/Reduction.lean (deg_eq_of_frobMatrix_data / deg_eq_of_frob_det_data, assuming per-prime matrix data). The latter reduction is ported in TauCeti.LinearAlgebra.Matrix.QuadraticFormCongruence. Here the pencil is formed in the morphism group of function-field isogenies, and its matrix data is proved, so the degree formula needs no additional witness or matrix-data hypotheses beyond the stated field and coefficient conditions.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.5, III.8 and V.1.

theorem TauCeti.Isogeny.Hom.zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_ne_zero {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (r s : ℤ) (hs : ↑s ≠ 0) : r • ofIsogeny (baseChangeFrobenius K W) - s • id (WeierstrassCurve.toAffine (W.baseChange K)) ≠ 0

If s is nonzero in the field, the Frobenius pencil r π - s is nonzero.

@[simp]

theorem TauCeti.Isogeny.Hom.isSeparable_toIsogeny_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id_iff {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (r s : ℤ) (h : r • ofIsogeny (baseChangeFrobenius K W) - s • id (WeierstrassCurve.toAffine (W.baseChange K)) ≠ 0) : Algebra.IsSeparable (↥(toIsogeny h).fieldPullback.fieldRange) (WeierstrassCurve.toAffine (W.baseChange K)).FunctionField ↔ ↑s ≠ 0

A nonzero Frobenius pencil r π - s is separable exactly when s is nonzero in the field.

theorem TauCeti.Isogeny.Hom.det_torsionLinearMap_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [DecidableEq K] [IsSepClosed K] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) (r s : ℤ) (hs : ↑s ≠ 0) : LinearMap.det ((r • ofIsogeny (baseChangeFrobenius K W) - s • id (WeierstrassCurve.toAffine (W.baseChange K))).torsionLinearMap N) = ↑(r • ofIsogeny (baseChangeFrobenius K W) - s • id (WeierstrassCurve.toAffine (W.baseChange K))).degree

Over a separably closed field in which N is invertible, the determinant of a Frobenius pencil on N-torsion is its degree modulo N, when s is nonzero in the field.

theorem TauCeti.Isogeny.Hom.degree_zsmul_ofIsogeny_baseChangeFrobenius_sub_zsmul_id {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 - (↑(Nat.card F) + 1 - ↑(id (WeierstrassCurve.toAffine (W.baseChange K)) - ofIsogeny (baseChangeFrobenius K W)).degree) * (r * s) + s ^ 2

Over a separably closed algebraic extension of the finite base, the degree of r π - s is the integral quadratic form with middle coefficient #F + 1 - deg (id - π), provided s is nonzero in the field.