The traces of the powers of Frobenius

Let W be an elliptic curve over a finite field F with q elements and π its q-power Frobenius endomorphism. This file defines the sequence

t n = q ^ n + 1 - deg (1 - π ^ n),

WeierstrassCurve.frobeniusPowTrace, and proves that it satisfies the linear recurrence

t 0 = 2, t 1 = a_q, t (n + 2) = a_q * t (n + 1) - q * t n,

where a_q = q + 1 - #W(F) is the Frobenius trace (Silverman V.2.3). For n ≥ 1, t n is the Frobenius trace of W over an extension of F of degree n, so the recurrence determines the point counts #W(𝔽_{qⁿ}) = q ^ n + 1 - t n over all finite extensions from the single number #W(F). Those counts are the coefficients of the logarithm of the zeta function Z(W/F, T) = exp (∑ #W(𝔽_{qⁿ}) Tⁿ / n), and the recurrence is what makes Z rational.

The sequence is defined through the degree of an endomorphism of W over F itself, so it needs no choice of a field with q ^ n elements, and the degree convention deg 0 = 0 gives t 0 = 2. Over a separably closed extension and for N prime to q, t n is the trace of π ^ n on E[N] modulo N: there π acts by a 2 × 2 matrix M over ZMod N with det M = q and det (1 - M ^ n) = deg (1 - π ^ n), and trace A = 1 + det A - det (1 - A) for a 2 × 2 matrix. The recurrence is then the Cayley–Hamilton theorem for M, read modulo every N prime to q.

Main definitions

• WeierstrassCurve.frobeniusPowTrace: the sequence t n = q ^ n + 1 - deg (1 - π ^ n).

Main results

• WeierstrassCurve.frobeniusPowTrace_zero, WeierstrassCurve.frobeniusPowTrace_one: t 0 = 2 and t 1 = a_q.
• WeierstrassCurve.frobeniusPowTrace_add_two: t (n + 2) = a_q * t (n + 1) - q * t n.
• WeierstrassCurve.frobeniusPowTrace_finrank: over a finite extension E/F of degree n, t n is the Frobenius trace of W over E.
• WeierstrassCurve.frobeniusPowTrace_eq_degree_baseChange: t n may be computed from the base-changed Frobenius over any extension of F.
• TauCeti.Isogeny.Hom.trace_torsionLinearMap_pow_ofIsogeny_baseChangeFrobenius: t n is the trace of π ^ n on E[N] modulo N, over a separably closed extension.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.8.6 and V.2.

noncomputable def WeierstrassCurve.frobeniusPowTrace {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] (n : ℕ) : ℤ

The trace of the nth power of Frobenius: q ^ n + 1 - deg (1 - π ^ n), for an elliptic curve W over a finite field with q elements and its q-power Frobenius endomorphism π.

At n = 0 it is 2, and for n ≥ 1 it is the Frobenius trace q ^ n + 1 - #W(𝔽_{qⁿ}) of W over an extension of degree n (frobeniusPowTrace_finrank). It satisfies the linear recurrence t (n + 2) = a_q * t (n + 1) - q * t n (frobeniusPowTrace_add_two).

theorem WeierstrassCurve.frobeniusPowTrace_def {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] (n : ℕ) : W.frobeniusPowTrace n = ↑(Nat.card F) ^ n + 1 - ↑(1 - TauCeti.Isogeny.Hom.ofIsogeny (TauCeti.Isogeny.frobeniusIsogeny W) ^ n).degree

The defining equation of frobeniusPowTrace.

@[simp]

theorem WeierstrassCurve.frobeniusPowTrace_zero {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] : W.frobeniusPowTrace 0 = 2

t 0 = 2: the zeroth power of Frobenius is the identity, and deg 0 = 0.

@[simp]

theorem WeierstrassCurve.frobeniusPowTrace_one {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] : W.frobeniusPowTrace 1 = W.frobeniusTrace

t 1 = a_q: the first term is the Frobenius trace, as deg (1 - π) = #W(F).

theorem WeierstrassCurve.frobeniusPowTrace_eq_degree_baseChange {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] (K : Type u_2) [Field K] [Algebra F K] (n : ℕ) : W.frobeniusPowTrace n = ↑(Nat.card F) ^ n + 1 - ↑(1 - TauCeti.Isogeny.Hom.ofIsogeny (TauCeti.Isogeny.baseChangeFrobenius K W) ^ n).degree

The trace of the nth power of Frobenius may be computed over any extension K of the finite base, from the base-changed Frobenius of W⁄K.

theorem WeierstrassCurve.frobeniusPowTrace_finrank {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] (E : Type u_2) [Field E] [Finite E] [Algebra F E] : W.frobeniusPowTrace (Module.finrank F E) = frobeniusTrace (Affine.baseChange W E)

Over an extension of degree n, the trace of the nth power of Frobenius is the Frobenius trace: t n = q ^ n + 1 - #W(E) for a finite extension E/F of degree n.

theorem TauCeti.Isogeny.Hom.trace_torsionLinearMap_pow_ofIsogeny_baseChangeFrobenius {F : Type u_1} {K : Type u_2} [Field F] [Finite F] [Field K] [Algebra F K] [IsSepClosed K] [DecidableEq K] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {N : ℕ} [NeZero N] (hN : ↑N ≠ 0) (n : ℕ) : (LinearMap.trace (ZMod N) ↥(AddSubgroup.torsionBy (WeierstrassCurve.toAffine (W.baseChange K)).Point ↑N)) ((ofIsogeny (baseChangeFrobenius K W) ^ n).torsionLinearMap N) = ↑(WeierstrassCurve.frobeniusPowTrace W n)

The trace of π ^ n on E[N] is t n modulo N, over a separably closed extension of the finite base in which N is invertible.

theorem WeierstrassCurve.frobeniusPowTrace_add_two {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve F) [W.IsElliptic] (n : ℕ) : W.frobeniusPowTrace (n + 2) = W.frobeniusTrace * W.frobeniusPowTrace (n + 1) - ↑(Nat.card F) * W.frobeniusPowTrace n

The recurrence for the traces of the powers of Frobenius: t (n + 2) = a_q * t (n + 1) - q * t n, where a_q is the Frobenius trace and q the number of elements of the base (Silverman V.2.3). With t 0 = 2 and t 1 = a_q, it determines every point count of W over a finite extension from #W(F).