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: Frobenius elements
▶
8.1
Status
8.2
Introduction and goal
8.3
Statement of the theorem
8.4
The extension \(B/A\).
8.5
The extension \((B/Q)/(A/P)\).
8.6
The extension \(L/K\).
9
Miniproject: Adeles
▶
9.1
Status
9.2
The goal
9.3
Local compactness
9.4
Base change
9.5
Discreteness and compactness
10
Miniproject: Haar Characters
▶
10.1
The goal
10.2
Initial definitions
10.3
Examples
10.4
Algebras
10.5
Left and right multiplication
10.6
Finite Products
10.7
Some measure-theoretic preliminaries
10.8
Restricted products
10.9
Adeles
11
Miniproject: Fujisaki’s Lemma
▶
11.1
The goal
11.2
Initial definitions
11.3
Enter the adeles
11.4
The proof
12
Miniproject: Quaternion algebras
▶
12.1
The goal
12.2
Initial definitions
12.3
Brief introduction to automorphic forms in this setting
12.4
Definition of spaces of automorphic forms
12.5
The main result
13
Miniproject: Hecke Operators
▶
13.1
Status
13.2
The goal
13.3
The abstract theory
13.4
Restricted products
13.5
Some local theory
13.6
Adelic groups
13.7
Automorphic forms
13.8
Concrete Hecke operators
13.9
Analysis of the Hecke algebra
14
Appendix: A collection of results which are needed in the proof.
▶
14.1
Results from class field theory
14.2
Structures on the points of an affine variety.
14.3
Algebraic groups.
14.4
Automorphic forms and representations
14.5
Galois representations
14.6
Algebraic geometry
14.7
Algebra
15
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
Chapter 14 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: Frobenius elements
8.1
Status
8.2
Introduction and goal
8.3
Statement of the theorem
8.4
The extension \(B/A\).
8.5
The extension \((B/Q)/(A/P)\).
8.6
The extension \(L/K\).
9
Miniproject: Adeles
9.1
Status
9.2
The goal
9.3
Local compactness
9.4
Base change
9.5
Discreteness and compactness
10
Miniproject: Haar Characters
10.1
The goal
10.2
Initial definitions
10.3
Examples
10.4
Algebras
10.5
Left and right multiplication
10.6
Finite Products
10.7
Some measure-theoretic preliminaries
10.8
Restricted products
10.9
Adeles
11
Miniproject: Fujisaki’s Lemma
11.1
The goal
11.2
Initial definitions
11.3
Enter the adeles
11.4
The proof
12
Miniproject: Quaternion algebras
12.1
The goal
12.2
Initial definitions
12.3
Brief introduction to automorphic forms in this setting
12.4
Definition of spaces of automorphic forms
12.5
The main result
13
Miniproject: Hecke Operators
13.1
Status
13.2
The goal
13.3
The abstract theory
13.4
Restricted products
13.5
Some local theory
13.6
Adelic groups
13.7
Automorphic forms
13.8
Concrete Hecke operators
13.9
Analysis of the Hecke algebra
14
Appendix: A collection of results which are needed in the proof.
14.1
Results from class field theory
14.2
Structures on the points of an affine variety.
14.3
Algebraic groups.
14.4
Automorphic forms and representations
14.5
Galois representations
14.6
Algebraic geometry
14.7
Algebra
15
Bibliography