1
Introduction
▶
1.1
Which proof is being formalised?
1.2
The structure of this blueprint
1.3
Remarks
2
First reductions of the problem
▶
2.1
Goal
2.2
Overview
2.3
Reduction to \(n\geq 5\) and prime
2.4
Frey packages
2.5
Galois representations and elliptic curves
2.6
The Frey curve
2.7
Reduction to two big theorems.
3
Reducibility of
p
-torsion of the Frey curve
▶
3.1
Overview
3.2
Hardly ramified representations
4
An overview of the proof
▶
4.1
Potential modularity.
4.2
A modularity lifting theorem
4.3
Compatible families, and reduction at 3
5
An example of an automorphic form
▶
5.1
Introduction
5.2
A quaternion algebra
5.3
\(\widehat{\mathbb {Z}}\)
5.4
More advanced remarks on \(\widehat{\mathbb {Z}}\) versus \(\mathbb {Q}\)
5.5
\(\widehat{\mathbb {Q}}\) and tensor products.
5.6
A crash course in tensor products
5.7
Additive structure of \(\widehat{\mathbb {Q}}\).
5.8
Multiplicative structure of the units of \(\widehat{\mathbb {Q}}\).
5.9
The Hurwitz quaternions
5.10
Profinite completion of the Hurwitz quaternions
6
Stating the modularity lifting theorems
▶
6.1
Automorphic forms and analysis
6.2
Central simple algebras
7
Automorphic forms and the Langlands Conjectures
▶
7.1
Definition of an automorphic form
7.2
The finite adeles of the rationals.
7.3
The adelic general linear group
7.4
Smooth functions
7.5
Slowly-increasing functions
7.6
Weights at infinity
7.7
The action of the universal enveloping algebra.
7.8
Automorphic forms
7.9
Hecke operators
8
Miniproject: Adeles
▶
8.1
Status
8.2
The goal
8.3
Local compactness
8.4
Base change
8.5
Discreteness and compactness
9
Miniproject: Haar Characters
▶
9.1
The goal
9.2
Initial definitions
9.3
Examples
9.4
Algebras
9.5
Left and right multiplication
9.6
Finite Products
9.7
Some measure-theoretic preliminaries
9.8
Restricted products
9.9
Adeles
10
Miniproject: Fujisaki’s Lemma
▶
10.1
The goal
10.2
Initial definitions
10.3
Enter the adeles
10.4
The proof
11
Miniproject: Quaternion algebras
▶
11.1
The goal
11.2
Initial definitions
11.3
Brief introduction to automorphic forms in this setting
11.4
Definition of spaces of automorphic forms
11.5
The main result
12
Miniproject: Hecke Operators
▶
12.1
Status
12.2
The goal
12.3
The abstract theory
12.4
Restricted products
12.5
Some local theory
12.6
Adelic groups
12.7
Automorphic forms
12.8
Concrete Hecke operators
12.9
Analysis of the Hecke algebra
13
Appendix: A collection of results which are needed in the proof.
▶
13.1
Results from class field theory
13.2
Structures on the points of an affine variety.
13.3
Algebraic groups.
13.4
Automorphic forms and representations
13.5
Galois representations
13.6
Algebraic geometry
13.7
Algebra
14
Bibliography
Chapter 1 graph
Chapter 2 graph
Chapter 3 graph
Chapter 4 graph
Chapter 5 graph
Chapter 6 graph
Chapter 7 graph
Chapter 8 graph
Chapter 9 graph
Chapter 10 graph
Chapter 11 graph
Chapter 12 graph
Chapter 13 graph
Towards a Lean proof of Fermat’s Last Theorem
Kevin Buzzard, Richard Taylor
1
Introduction
1.1
Which proof is being formalised?
1.2
The structure of this blueprint
1.3
Remarks
2
First reductions of the problem
2.1
Goal
2.2
Overview
2.3
Reduction to \(n\geq 5\) and prime
2.4
Frey packages
2.5
Galois representations and elliptic curves
2.6
The Frey curve
2.7
Reduction to two big theorems.
3
Reducibility of
p
-torsion of the Frey curve
3.1
Overview
3.2
Hardly ramified representations
4
An overview of the proof
4.1
Potential modularity.
4.2
A modularity lifting theorem
4.3
Compatible families, and reduction at 3
5
An example of an automorphic form
5.1
Introduction
5.2
A quaternion algebra
5.3
\(\widehat{\mathbb {Z}}\)
5.4
More advanced remarks on \(\widehat{\mathbb {Z}}\) versus \(\mathbb {Q}\)
5.5
\(\widehat{\mathbb {Q}}\) and tensor products.
5.6
A crash course in tensor products
5.7
Additive structure of \(\widehat{\mathbb {Q}}\).
5.8
Multiplicative structure of the units of \(\widehat{\mathbb {Q}}\).
5.9
The Hurwitz quaternions
5.10
Profinite completion of the Hurwitz quaternions
6
Stating the modularity lifting theorems
6.1
Automorphic forms and analysis
6.2
Central simple algebras
7
Automorphic forms and the Langlands Conjectures
7.1
Definition of an automorphic form
7.2
The finite adeles of the rationals.
7.3
The adelic general linear group
7.4
Smooth functions
7.5
Slowly-increasing functions
7.6
Weights at infinity
7.7
The action of the universal enveloping algebra.
7.8
Automorphic forms
7.9
Hecke operators
8
Miniproject: Adeles
8.1
Status
8.2
The goal
8.3
Local compactness
8.4
Base change
8.5
Discreteness and compactness
9
Miniproject: Haar Characters
9.1
The goal
9.2
Initial definitions
9.3
Examples
9.4
Algebras
9.5
Left and right multiplication
9.6
Finite Products
9.7
Some measure-theoretic preliminaries
9.8
Restricted products
9.9
Adeles
10
Miniproject: Fujisaki’s Lemma
10.1
The goal
10.2
Initial definitions
10.3
Enter the adeles
10.4
The proof
11
Miniproject: Quaternion algebras
11.1
The goal
11.2
Initial definitions
11.3
Brief introduction to automorphic forms in this setting
11.4
Definition of spaces of automorphic forms
11.5
The main result
12
Miniproject: Hecke Operators
12.1
Status
12.2
The goal
12.3
The abstract theory
12.4
Restricted products
12.5
Some local theory
12.6
Adelic groups
12.7
Automorphic forms
12.8
Concrete Hecke operators
12.9
Analysis of the Hecke algebra
13
Appendix: A collection of results which are needed in the proof.
13.1
Results from class field theory
13.2
Structures on the points of an affine variety.
13.3
Algebraic groups.
13.4
Automorphic forms and representations
13.5
Galois representations
13.6
Algebraic geometry
13.7
Algebra
14
Bibliography