FLT/Slop/PGL2/FiniteSubgroups/DicksonClassification.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Dickson's classification of the finite subgroups of PGL₂(𝔽̄_p)
The main theorem Dickson.dickson_classification: for p an odd prime, every finite
subgroup of PGL₂(𝔽̄_p) is one of:
- cyclic;
- dihedral of order
2n,n ≥ 2; - isomorphic to
A₄,S₄orA₅; - a semidirect product of an elementary abelian
p-group by a cyclic group of order prime top; - isomorphic to
PSL₂(𝔽_{p^m})orPGL₂(𝔽_{p^m})for somem ≥ 1.
This is the combination of the tame case (Dickson.classification_tame_slop, order
coprime to p) and the wild case (Dickson.classification_wild_slop, order divisible
by p).
This classification (due to Dickson, 1901) is used in the proof of Fermat's Last
Theorem to analyse the image of the mod-p Galois representations attached to the
Frey curve.
Imports (2)
Imported by 2 files
- theorem
Dickson.dickson_classificationline 54 sourcestandard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses:
Nat,Fact,Nat.Prime,GT.gt,OfNat.ofNat,Subgroup, Dickson.PGLOf, Dickson.K,ZMod,Matrix.GeneralLinearGroup,Fin,Matrix,Subgroup.center,Finite,Subtype,Membership.mem,Or,IsCyclic,Exists,Andand 18 moreProof uses:
dite,Nontrivial,Nat.card,Eq, Dickson.classification_wild_slop,Or.inr,Or.inl,Not,Fintype,Fintype.ofFinite, Dickson.classification_tame_slop,Subsingleton,Iff.mp,not_nontrivial_iff_subsingleton,IsCyclic.mk,Exists.intro,Function.Surjective,Int,Eq.mpr,idand 3 more119 instances, coercions and auxiliary constants left out.
Tactic trace: 31 steps
Open to load the checked before-and-after goal states.