Torsion points E[ℓ]

The points killed by ℓ-fold addition keep the curve’s arithmetic in a finite cage.

Start with a concrete example

Turn a dial by a quarter turn. Four repetitions return it to its start. “Torsion” similarly concerns points that return to zero after a fixed number of additions, using the curve’s addition rule.

A small check: try the idea

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

A quarter turn returns to the start after how many repetitions?

Read the answer and reasoning

4. Four quarter turns make one full turn. The curve uses its own addition rule, but this illustrates returning after a fixed number of repeats.

Build the idea in three steps

The curve addition has a clock trick of its own: take a point P and add it to itself again and again. If after ℓ steps the walk returns to zero, P is a torsion point — and the ℓ-torsion part is the collection of points passing that test.
Submodule.torsionBy ℤ (W'.Point) ℓ is the Lean definition: the points with ℓ • P = 0. For the prime exponent of this proof, that world is E[ℓ], and it is small: the Frey curve hands exactly this finite cage over to the symmetries.
The lemma proves nobody escapes: if P is ℓ-torsion, then so is σ • P, because σ • (m • P) = m • (σ • P) — the last line rewrites the walk through map_zsmul and lands on zero again. You can shuffle the cage, you cannot open it.

A small example

On the unit circle viewed as a group under multiplication, fixing a positive integer ℓ gives exactly ℓ roots of z^ℓ = 1. For ℓ = 4 these are 1, i, −1 and −i. The union of the roots for all positive ℓ is infinite. A fixed torsion level and all torsion points are different sets.

Use in Lean · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_GaloisRep.lean

43lemma smul_mem_torsionBy {n : ℕ} (σ : K ≃ₐ[S] K) {P : (W'⁄K).Point}44    (hP : P ∈ Submodule.torsionBy ℤ (W'⁄K).Point n) :45    σ • P ∈ Submodule.torsionBy ℤ (W'⁄K).Point n := by46  rw [Submodule.mem_torsionBy_iff] at hP ⊢47  rw [← algEquiv_smul_zsmul, hP, smul_zero]

How to read this Lean

The five lines are silent about the group law — they rely on it through the types (Point already carries +) and through map_zsmul, the guarantee that integer multiples commute with a symmetry. The next pages bundle exactly this: the number world symmetries acting inside E[ℓ]. The set of points stays fixed while its members swap — the seed of the Galois representation.

Original source ↗ · L43–47 Open the complete saved source

Where this idea is used

6. The scissors incident 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

Torsion points E[ℓ]

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · 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