Counting points: the curve’s number at a prime

Reduce the curve modulo a prime and count that finite point set.

Start with a concrete example

For y²=x³−x using remainders 0,…,4, the five x values allow 1,1,2,2,1 choices of y. That is 7 ordinary points, plus one point at infinity: 8 total. The recorded number is 5+1−8=−2.

A small check: try the idea

Think with the concrete example above. You can try again.

In the example with 8 points over the five-element setting, what is 5+1−8?

Read the answer and reasoning

−2. The trace combines the field size with the point count. It is not the point count itself: 6−8=−2.

Build the idea in three steps

Every quantity the duet compares must be defined somewhere: a cusp form gives its coefficients, and the curve must give its own numbers. This page is where the curve’s numbers enter.
To read a curve’s arithmetic at a prime ℓ, reduce the curve modulo ℓ into ZMod ℓ and observe the reduced curve’s points. Counting them is an ordinary finite task.
Lean names the composed quantity apOfModel: reductionMod p sends the integer coefficients to ZMod p, and that reduction’s traceOfFrobenius combines the residue field’s size with the counted points. The classifier IsGoodPrimeFor forbids primes dividing Δ — at those primes the reduced curve behaves differently.

A small example

For y² = x³ − x over the five residues, the numbers of y-values at x = 0, 1, 2, 3, 4 are 1, 1, 2, 2, 1. That is 7 affine points, plus the point at infinity: #E(𝔽₅) = 8. Thus the trace is 5 + 1 − 8 = −2, not the raw point count.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

72def traceOfFrobenius : ℤ := (Nat.card F : ℤ) + 1 - (W.card : ℤ)73 74end Card75 76def reductionMod (W : WeierstrassCurve ℤ) (p : ℕ) : WeierstrassCurve (ZMod p) :=77  W.map (Int.castRingHom (ZMod p))78 79def apOfModel (W : WeierstrassCurve ℤ) (p : ℕ) : ℤ :=

How to read this Lean

W.toAffine.Point includes nonsingular affine points and the identity at infinity, despite the word Affine in the name. At a good prime p all points of the reduced curve are nonsingular, and traceOfFrobenius is p + 1 minus that complete point count. reductionMod and apOfModel compose this calculation for an integral model.

Original source ↗ · L72–79 Open the complete saved source

Where this idea is used

8. The secret duet 9. Two doors to the concert 10. A three-note audition 11. Borrow a better passport 12. The workshops agree 13. Pip’s impossible quilt 14. The shrinking reservation

Counting points: the curve’s number at a prime

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue