1
Abstract and Acknowledgements
2
Introduction
▶
2.1
What is the formalization of mathematics?
▶
What is Lean?
2.2
Fermat’s Last Theorem
2.3
Formalizing Fermat’s Last Theorem
2.4
Classification of finite subgroups of the \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\)
3
Preliminaries
▶
3.1
Some Elementary Theorems
3.2
Sylow Theory
3.3
Group Action
3.4
Conjugation
3.5
Automorphism
3.6
Direct Product
4
Reduction of classification of finite subgroups of \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\) to classification of finite subgroups of \(\operatorname{PSL}_2(\bar{\mathbb {F}}_p)\)
▶
4.1
Over an algebraically closed field \(\operatorname{PSL}_n(F)\) is isomorphic to the projective \(\operatorname{PGL}_n(F)\)
4.2
Christopher Butler’s exposition
5
Properties of the two dimensional \(\operatorname{SL}_2(F)\)
▶
5.1
General Notation
5.2
Subsets of \(L\)
▶
Special matrices of \(\operatorname{SL}_2(F)\)
Special subgroups of \(\operatorname{SL}_2(F)\)
5.3
The Centre of \(L\)
5.4
Conjugacy of the Elements of \(L\)
5.5
Centralisers & Normalisers
5.6
The Projective Line & Triple Transitivity
6
The Maximal Abelian Subgroup Class Equation
▶
6.1
A finite subgroup of \(L\)
6.2
Maximal Abelian Subgroups
6.3
Conjugacy of Maximal Abelian Subgroups
6.4
Constructing The Class Equation
7
Dickson’s Classification Theorem for finite subgroups of \(\operatorname{SL}_2(F)\)
▶
7.1
Five Lemmas
7.2
The Six Cases
7.3
Dickson’s Classification Theorem
8
Bibliography
Dependency graph
Classification of finite subgroups of PGL
AlexBrodbelt
1
Abstract and Acknowledgements
2
Introduction
2.1
What is the formalization of mathematics?
What is Lean?
2.2
Fermat’s Last Theorem
2.3
Formalizing Fermat’s Last Theorem
2.4
Classification of finite subgroups of the \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\)
3
Preliminaries
3.1
Some Elementary Theorems
3.2
Sylow Theory
3.3
Group Action
3.4
Conjugation
3.5
Automorphism
3.6
Direct Product
4
Reduction of classification of finite subgroups of \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\) to classification of finite subgroups of \(\operatorname{PSL}_2(\bar{\mathbb {F}}_p)\)
4.1
Over an algebraically closed field \(\operatorname{PSL}_n(F)\) is isomorphic to the projective \(\operatorname{PGL}_n(F)\)
4.2
Christopher Butler’s exposition
5
Properties of the two dimensional \(\operatorname{SL}_2(F)\)
5.1
General Notation
5.2
Subsets of \(L\)
Special matrices of \(\operatorname{SL}_2(F)\)
Special subgroups of \(\operatorname{SL}_2(F)\)
5.3
The Centre of \(L\)
5.4
Conjugacy of the Elements of \(L\)
5.5
Centralisers & Normalisers
5.6
The Projective Line & Triple Transitivity
6
The Maximal Abelian Subgroup Class Equation
6.1
A finite subgroup of \(L\)
6.2
Maximal Abelian Subgroups
6.3
Conjugacy of Maximal Abelian Subgroups
6.4
Constructing The Class Equation
7
Dickson’s Classification Theorem for finite subgroups of \(\operatorname{SL}_2(F)\)
7.1
Five Lemmas
7.2
The Six Cases
7.3
Dickson’s Classification Theorem
8
Bibliography