Isogenous elliptic curves over a finite field have the same number of points

Let φ : W₁ → W₂ be an isogeny of elliptic curves over a finite field F with q elements, and let π₁, π₂ be their q-power Frobenius endomorphisms. Frobenius commutes with every isogeny defined over F, so φ ∘ π₁ ^ n = π₂ ^ n ∘ φ, and composition is biadditive, so

φ ∘ (1 - π₁ ^ n) = (1 - π₂ ^ n) ∘ φ.

The degree is multiplicative and deg φ ≠ 0, hence deg (1 - π₁ ^ n) = deg (1 - π₂ ^ n) for every n. For n = 1 both sides are point counts, deg (1 - π) = #E(𝔽_q), which gives the classical statement that isogenous curves over 𝔽_q have the same number of points. For general n both sides are point counts over an extension of F of degree n, and they are the coefficients of the logarithm of the zeta function, so isogenous curves have the same zeta function.

Over the fraction field of a discrete valuation ring with finite residue field, the local polynomial of a curve with good reduction (Mathlib's WeierstrassCurve.localPolynomial, the local factor of the L-function) is 1 - a T + q T², with a the Frobenius trace of the reduction. So two curves with good reduction whose reductions are isogenous have the same local polynomial. The reduction of an isogeny defined over the fraction field to an isogeny of the reduced curves is not constructed here; it is supplied as the isogeny of reductions.

Main results

• TauCeti.Isogeny.degree_one_sub_frobenius_pow_eq: deg (1 - π₁ ^ n) = deg (1 - π₂ ^ n).
• TauCeti.Isogeny.pointCount_eq: isogenous curves over a finite field have the same number of points, the point at infinity included.
• TauCeti.Isogeny.frobeniusTrace_eq: they have the same Frobenius trace a_q.
• TauCeti.Isogeny.frobeniusPowTrace_eq: they have the same traces of the powers of Frobenius.
• TauCeti.Isogeny.pointCount_baseChange_eq: they have the same number of points over every finite extension of F.
• TauCeti.Isogeny.zetaFunction_eq: they have the same zeta function.
• TauCeti.Isogeny.localPolynomial_eq: two curves with good reduction whose reductions are isogenous have the same local polynomial.

References

• J. Silverman, The Arithmetic of Elliptic Curves, V.1–2.

theorem TauCeti.Isogeny.degree_one_sub_frobenius_pow_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (n : ℕ) : (1 - Hom.ofIsogeny (frobeniusIsogeny W₁) ^ n).degree = (1 - Hom.ofIsogeny (frobeniusIsogeny W₂) ^ n).degree

Isogenous curves have the same deg (1 - π ^ n): if φ : W₁ → W₂ is an isogeny over a finite field, then deg (1 - π₁ ^ n) = deg (1 - π₂ ^ n) for the Frobenius endomorphisms π₁ of W₁ and π₂ of W₂.

theorem TauCeti.Isogeny.pointCount_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : WeierstrassCurve.pointCount W₁ = WeierstrassCurve.pointCount W₂

Isogenous curves over a finite field have the same number of points, the point at infinity included.

theorem TauCeti.Isogeny.frobeniusTrace_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : WeierstrassCurve.frobeniusTrace W₁ = WeierstrassCurve.frobeniusTrace W₂

Isogenous curves over a finite field have the same Frobenius trace a_q = q + 1 - #E(𝔽_q).

theorem TauCeti.Isogeny.frobeniusPowTrace_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (n : ℕ) : WeierstrassCurve.frobeniusPowTrace W₁ n = WeierstrassCurve.frobeniusPowTrace W₂ n

Isogenous curves over a finite field have the same traces of the powers of Frobenius q ^ n + 1 - deg (1 - π ^ n).

theorem TauCeti.Isogeny.pointCount_baseChange_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (E : Type u_2) [Field E] [Finite E] [Algebra F E] : (WeierstrassCurve.baseChange W₁ E).pointCount = (WeierstrassCurve.baseChange W₂ E).pointCount

Isogenous curves over a finite field have the same number of points over every finite extension E of the base, the point at infinity included.

theorem TauCeti.Isogeny.zetaFunction_eq {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : WeierstrassCurve.zetaFunction W₁ = WeierstrassCurve.zetaFunction W₂

Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n).

theorem TauCeti.Isogeny.localPolynomial_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Finite (IsLocalRing.ResidueField R)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W₁ W₂ : WeierstrassCurve K} (φ : Isogeny (WeierstrassCurve.reduction R (WeierstrassCurve.minimal R W₁)).toAffine (WeierstrassCurve.reduction R (WeierstrassCurve.minimal R W₂)).toAffine) (h₁ : WeierstrassCurve.HasGoodReduction R (WeierstrassCurve.minimal R W₁)) (h₂ : WeierstrassCurve.HasGoodReduction R (WeierstrassCurve.minimal R W₂)) : WeierstrassCurve.localPolynomial R W₁ = WeierstrassCurve.localPolynomial R W₂

Curves with good reduction and isogenous reductions have the same local polynomial: over the fraction field of a discrete valuation ring with finite residue field, if W₁ and W₂ have good reduction and there is an isogeny between their reductions, then their local factors 1 - a T + q T² (Mathlib's WeierstrassCurve.localPolynomial) agree.