Galois representations

Encode number-preserving symmetries as transformations of vectors.

Start with a concrete example

Imagine recording each symmetry of an object as instructions for moving arrows. Doing two symmetries in succession must match doing the two recorded arrow moves. That rule of correspondence matters, not just assigning a label.

A small check: try the idea

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

Must recording two successive symmetries agree with doing their two recorded arrow moves?

Read the answer and reasoning

Yes; composition must be respected. A representation records actions consistently with their composition. Merely naming each symmetry does not supply that consistency.

Build the idea in three steps

Start with arithmetic symmetries: rearrangements of an extension of the rational numbers that preserve arithmetic and fix rational numbers.
Curve points have an addition operation. The points killed by multiplication by p form the p-torsion; at a prime this has linear structure over residues.
The arithmetic symmetries act on these points. Recording their action as linear transformations is the representation used in this proof.

A small example

“Mod-three representation” concerns an action on three-torsion data. It does not mean checking three sample points.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_GaloisRep.lean

49noncomputable instance instSMulTorsionBy (n : ℕ) :50    SMul (K ≃ₐ[S] K) (Submodule.torsionBy ℤ (W'⁄K).Point n) :=51  ⟨fun σ P => ⟨σ • (P : (W'⁄K).Point), smul_mem_torsionBy σ P.property⟩⟩

How to read this Lean

Submodule.torsionBy selects points killed by n. σ is an arithmetic symmetry and • denotes its action on a point.

Original source ↗ · L49–51 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

Galois representations

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