University
No nonzero proper subspace is preserved by every allowed symmetry.
Draw a line through the center of a flat sheet. Rotate the sheet by 90°. The line moves to a different line. Change its starting angle: does any line stay the same?
Starting angle 0°. The rotated line is different.
This example uses lines in a real plane and a 90° rotation. The representation in the proof lives in its specified field; changing the field can change irreducibility.
Compare the numbers in the question with the diagram you are moving. You can try again.
Set the starting angle to 0°. The solid and dashed lines share the center, but their sets of points differ. This is only the real-plane model.
Your answer fits this explanation. Look for the same idea in the comic.
No; it becomes a vertical line. Set the starting angle to 0°. The solid and dashed lines share the center, but their sets of points differ. This is only the real-plane model.
A line preserved by every action would be a forbidden proper nonzero subspace. A line preserved by just one action is not enough to violate irreducibility.
FLT · aa2d8b3 · Def_FLTPrelim_GaloisRep.lean
def GaloisRepIsIrreducible (W' : Affine R) (n : ℕ) : Prop :=Nontrivial (Submodule.torsionBy ℤ (W'⁄K).Point n) ∧∀ N : Submodule (ZMod n) (Submodule.torsionBy ℤ (W'⁄K).Point n),IsGaloisStable S N → N = ⊥ ∨ N = ⊤
Nontrivial excludes the zero-only space. The alternatives N = ⊥ ∨ N = ⊤ say N is zero or the whole space.
Irreducibility
Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.
No nonzero proper subspace is preserved by every allowed symmetry.
Earlier ideas are listed under “Start with these ideas” on this page.
A line preserved by every action would be a forbidden proper nonzero subspace. A line preserved by just one action is not enough to violate irreducibility.
Close this panel to return to the exact place you were reading. These are prepared hints for this page.
Start with the first small story →