Point counts and Frobenius traces
DefinitionFrobenius trace#✓fully proved
Let \(W\) be a Weierstrass curve over a finite field \(F\) with \(q\) elements, and let \(\#W(F)\) be the number of nonsingular \(F\)-points of \(W\), counting the point at infinity. The Frobenius trace of \(W\) is the integer \(a_q(W) = q + 1 - \#W(F)\).
TheoremPoint count from affine solutions#✓fully proved
Let \(W\) be an elliptic curve in Weierstrass form over a finite field \(F\). The number of \(F\)-points of \(W\), counting the point at infinity, is one more than the number of pairs \((x, y) \in F \times F\) satisfying the Weierstrass equation of \(W\).
TheoremUpper bound on the point count#✓fully proved
Let \(W\) be a Weierstrass curve over a finite field \(F\) with \(q\) elements. The number of nonsingular \(F\)-points of \(W\), counting the point at infinity, is at most \(2q + 1\).
Each \(x \in F\) lies under at most two affine points, since the Weierstrass equation is quadratic in \(y\).
TheoremPoint count from the Frobenius trace#✓fully proved
Let \(W\) be a Weierstrass curve over a finite field \(F\) with \(q\) elements, and let \(\#W(F)\) be the number of nonsingular \(F\)-points of \(W\), counting the point at infinity. Then \(\#W(F) = q + 1 - a_q(W)\), where \(a_q(W)\) is the Frobenius trace of \(W\).
theorem natCard_point_eq_natCard_add_one_sub_frobeniusTrace [Finite F] :
(Nat.card W.Point : ℤ) = (Nat.card F : ℤ) + 1 - W.frobeniusTraceUses 1
TheoremPoint count plus Frobenius trace#✓fully proved
Let \(W\) be a Weierstrass curve over a finite field \(F\) with \(q\) elements, and let \(\#W(F)\) be the number of nonsingular \(F\)-points of \(W\), counting the point at infinity. Then \(\#W(F) + a_q(W) = q + 1\), where \(a_q(W)\) is the Frobenius trace of \(W\).
theorem natCard_point_add_frobeniusTrace_eq [Finite F] :
(Nat.card W.Point : ℤ) + W.frobeniusTrace = (Nat.card F : ℤ) + 1Uses 1
TheoremWaterhouse's theorem on Frobenius traces#●ready to prove
Let \(p\) be a prime, let \(a \ge 1\), and let \(F\) be a finite field with \(q = p^a\) elements. An integer \(\beta\) is the Frobenius trace \(q + 1 - \#E(F)\) of some elliptic curve \(E\) over \(F\) if and only if \(\beta^2 \le 4q\) and one of the following holds: 1. \(\gcd(\beta, p) = 1\); 2. \(a\) is even and \(\beta = \pm 2p^{a/2}\); 3. \(a\) is even, \(p \not\equiv 1 \pmod 3\) and \(\beta = \pm p^{a/2}\); 4. \(a\) is odd, \(p = 2\) or \(p = 3\), and \(\beta = \pm p^{(a+1)/2}\); 5. \(a\) is odd, or \(a\) is even and \(p \not\equiv 1 \pmod 4\), and \(\beta = 0\).
The paper states a one-to-one correspondence between \(F\)-isogeny classes of elliptic curves and these integers; the statement above describes its image. Injectivity is Tate's isogeny theorem.
public theorem_wanted exists_isElliptic_frobeniusTrace_eq_iff {F : Type*} [Field F]
[Finite F] {p a : ℕ} (hp : p.Prime) (ha : 0 < a) (hq : Nat.card F = p ^ a) (β : ℤ) :
(∃ W : WeierstrassCurve F, W.IsElliptic ∧ W.toAffine.frobeniusTrace = β) ↔
β ^ 2 ≤ 4 * (p : ℤ) ^ a ∧
(Int.gcd β p = 1 ∨
(Even a ∧ (β = 2 * (p : ℤ) ^ (a / 2) ∨ β = -(2 * (p : ℤ) ^ (a / 2)))) ∨
(Even a ∧ ¬ p ≡ 1 [MOD 3] ∧ (β = (p : ℤ) ^ (a / 2) ∨ β = -(p : ℤ) ^ (a / 2))) ∨
(Odd a ∧ (p = 2 ∨ p = 3) ∧
(β = (p : ℤ) ^ ((a + 1) / 2) ∨ β = -(p : ℤ) ^ ((a + 1) / 2))) ∨
((Odd a ∨ (Even a ∧ ¬ p ≡ 1 [MOD 4])) ∧ β = 0))Sources
- Daniel Vallières, Elliptic Curves over Finite Fields and Ramanujan Graphs on Two Vertices, INTEGERS 24 (2024), Article A8, Theorem 6.
Uses 1
TheoremIhara's criterion for Ramanujan graphs#●ready to prove
Let \(q \ge 2\) be a natural number and let \(A\) be a symmetric \(n \times n\) matrix with integer entries. Every complex root \(\mu \ne q + 1\) of the characteristic polynomial of \(A\) satisfies \(|\mu| \le 2\sqrt{q}\) if and only if, for every such root \(\mu \ne q + 1\), every complex number \(s\) with \(1 - \mu q^{-s} + q^{1 - 2s} = 0\) has real part \(1/2\).
When \(A\) is the adjacency matrix of a \((q + 1)\)-regular graph \(X\), the left side says that \(X\) is Ramanujan. Writing \(\zeta_X\) for the Ihara zeta function of \(X\), the numbers \(s\) on the right are the non-trivial zeros of \(Q_X(s) = \zeta_X(q^{-s})^{-1}\), that is, the zeros of \(P_X(q^{-s}) = \prod_{\mu \ne q + 1} (1 - \mu q^{-s} + q^{1 - 2s})\). The roots \(\mu\) are real because \(A\) is symmetric. The paper also assumes that \(X\) is connected and regular and has at least two vertices; these assumptions are not needed, since the equivalence holds root by root.
public theorem_wanted ramanujan_iff_nontrivial_zeros_re_eq_half {n q : ℕ} (hq : 2 ≤ q)
(A : Matrix (Fin n) (Fin n) ℤ) (hA : A.IsSymm) :
(∀ μ ∈ A.charpoly.aroots ℂ, μ ≠ (q : ℂ) + 1 → ‖μ‖ ≤ 2 * Real.sqrt q) ↔
∀ μ ∈ A.charpoly.aroots ℂ, μ ≠ (q : ℂ) + 1 → ∀ s : ℂ,
1 - μ * (q : ℂ) ^ (-s) + (q : ℂ) ^ (1 - 2 * s) = 0 → s.re = 1 / 2Sources
- Daniel Vallières, Elliptic Curves over Finite Fields and Ramanujan Graphs on Two Vertices, INTEGERS 24 (2024), Article A8, Theorem 2.
TheoremRamanujan graphs give Weil numbers#●ready to prove
Let \(q\) be a natural number and let \(A\) be a symmetric \(n \times n\) matrix with integer entries such that every complex root \(\mu \ne q + 1\) of its characteristic polynomial satisfies \(|\mu| \le 2\sqrt{q}\). Let \(\mu \ne q + 1\) be a complex root of the characteristic polynomial of \(A\) and let \(\alpha \in \mathbb{C}\) satisfy \(\alpha^2 - \mu\alpha + q = 0\). Then \(\alpha\) is an algebraic integer, and every complex root of the minimal polynomial of \(\alpha\) over \(\mathbb{Q}\) has absolute value \(\sqrt{q}\); that is, \(\alpha\) is a Weil \(q\)-number.
When \(A\) is the adjacency matrix of a \((q + 1)\)-regular graph \(X\), the hypothesis says that \(X\) is Ramanujan, and the numbers \(\alpha\) are the inverse roots of \(P_X(u) = \prod_{\mu \ne q + 1} (1 - \mu u + q u^2)\). The paper takes \(q = p^a\) and \(X\) connected; neither assumption is needed.
public theorem_wanted isWeilNumber_of_ramanujan {n q : ℕ} (A : Matrix (Fin n) (Fin n) ℤ)
(hA : A.IsSymm)
(hram : ∀ μ ∈ A.charpoly.aroots ℂ, μ ≠ (q : ℂ) + 1 → ‖μ‖ ≤ 2 * Real.sqrt q)
{μ α : ℂ} (hμ : μ ∈ A.charpoly.aroots ℂ) (hμq : μ ≠ (q : ℂ) + 1)
(hα : α ^ 2 - μ * α + q = 0) :
IsIntegral ℤ α ∧ ∀ β ∈ (minpoly ℚ α).aroots ℂ, ‖β‖ = Real.sqrt qSources
- Daniel Vallières, Elliptic Curves over Finite Fields and Ramanujan Graphs on Two Vertices, INTEGERS 24 (2024), Article A8, Proposition 1.
TheoremElliptic curves with point count divisible by 4 and Ramanujan graphs on two vertices#●ready to prove
Let \(p\) be an odd prime, let \(a \in \{1, 2\}\), and let \(F\) be a finite field with \(q = p^a\) elements. A natural number \(N\) is the number \(\#E(F)\) of \(F\)-points (counting the point at infinity) of some elliptic curve \(E\) over \(F\) with \(4 \mid N\) if and only if there are natural numbers \(l\) and \(m\) with \(N = 2m\), \(2l + m = q + 1\), \(m > 0\) and \((2l - m)^2 \le 4q\).
In graph terms, \(X(l, m)\) is the two-vertex graph with \(l\) loops at each vertex and \(m\) edges between the two vertices. For such \(l\) and \(m\) it is \((q + 1)\)-regular, it is connected exactly when \(m > 0\), and its non-trivial eigenvalue is \(2l - m\), so the last condition says that \(X(l, m)\) is Ramanujan. The paper states a bijection from \(F\)-isogeny classes of such curves to these graphs; the statement above is its point-count form, and injectivity on isogeny classes is Tate's theorem.
public theorem_wanted exists_isElliptic_card_eq_iff_ramanujan_two_vertices {F : Type*} [Field F]
[Finite F] {p a : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) (ha : a = 1 ∨ a = 2)
(hq : Nat.card F = p ^ a) (N : ℕ) :
(∃ W : WeierstrassCurve F, W.IsElliptic ∧ Nat.card W.toAffine.Point = N ∧ 4 ∣ N) ↔
∃ l m : ℕ, N = 2 * m ∧ 2 * l + m = p ^ a + 1 ∧ 0 < m ∧
((2 * l : ℤ) - m) ^ 2 ≤ 4 * (p : ℤ) ^ aSources
- Daniel Vallières, Elliptic Curves over Finite Fields and Ramanujan Graphs on Two Vertices, INTEGERS 24 (2024), Article A8, Theorem 8.
TheoremOrdinary elliptic curves with point count divisible by 4 and Ramanujan graphs on two vertices#●ready to prove
Ordinary elliptic curves with point count divisible by 4 and Ramanujan graphs on two vertices. Let \(p\) be an odd prime, let \(a \ge 1\), and let \(F\) be a finite field with \(q = p^a\) elements. A natural number \(N\) is the number \(\#E(F)\) of \(F\)-points (counting the point at infinity) of some elliptic curve \(E\) over \(F\) with \(4 \mid N\) whose Frobenius trace \(q + 1 - \#E(F)\) is coprime to \(p\) if and only if there are natural numbers \(l\) and \(m\) with \(N = 2m\), \(2l + m = q + 1\), \(m > 0\), \((2l - m)^2 \le 4q\) and \(2m \not\equiv 1 \pmod p\).
A Frobenius trace coprime to \(p\) is the paper's criterion for \(E\) to be ordinary; since \(p \mid q\), the trace \(q + 1 - 2m\) is coprime to \(p\) exactly when \(2m \not\equiv 1 \pmod p\). In graph terms, \(X(l, m)\) is the two-vertex graph with \(l\) loops at each vertex and \(m\) edges between the two vertices; it is \((q + 1)\)-regular, connected exactly when \(m > 0\), and Ramanujan exactly when \((2l - m)^2 \le 4q\). The paper states a bijection from \(F\)-isogeny classes of such curves to these graphs; the statement above is its point-count form, and injectivity on isogeny classes is Tate's theorem.
public theorem_wanted exists_ordinary_card_eq_iff_ramanujan_two_vertices {F : Type*} [Field F]
[Finite F] {p a : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) (ha : 0 < a)
(hq : Nat.card F = p ^ a) (N : ℕ) :
(∃ W : WeierstrassCurve F, W.IsElliptic ∧ Int.gcd W.toAffine.frobeniusTrace p = 1 ∧
Nat.card W.toAffine.Point = N ∧ 4 ∣ N) ↔
∃ l m : ℕ, N = 2 * m ∧ 2 * l + m = p ^ a + 1 ∧ 0 < m ∧
((2 * l : ℤ) - m) ^ 2 ≤ 4 * (p : ℤ) ^ a ∧ ¬ 2 * m ≡ 1 [MOD p]Sources
- Daniel Vallières, Elliptic Curves over Finite Fields and Ramanujan Graphs on Two Vertices, INTEGERS 24 (2024), Article A8, Theorem 9.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.