Introduction

The key ingredient in Wiles' proof of Fermat's Last Theorem is a modularity lifting theorem, sometimes called an \(R=T\) theorem. For Wiles, the \(R\) came from elliptic curves, the \(T\) came from classical modular forms, and the fact that they're equal is basically the Shimura–Taniyama–Weil conjecture, now known as the Breuil–Conrad–Diamond–Taylor modularity theorem: any elliptic curve over the rationals is modular.

At the heart of the proof we shall formalise is also an \(R=T\) theorem, however the \(T\) which we shall use will be associated not to classical modular forms, but to spaces of more general automorphic forms called quaternionic modular forms. Those of you who know something about classical modular forms might well know that the groups \(\operatorname{SL}_2(\mathbb{R})\) and \(\operatorname{SL}_2(\mathbb{Z})\) are intimately involved; these are the norm 1 units in the matrix rings \(M_2(\mathbb{R})\) and \(M_2(\mathbb{Z})\). In the theory of quaternionic modular forms, the analogous groups are the norm 1 units in rings such as Hamilton's quaternions \(\mathbb{R}\oplus\mathbb{R} i\oplus\mathbb{R} j\oplus\mathbb{R} k\), and subrings such as \(\mathbb{Z}\oplus\mathbb{Z} i\oplus\mathbb{Z} j\oplus\mathbb{Z} k\).

One of the main goals of the FLT project at the time of writing this sentence, is formalising the statement of the modularity lifting theorem which we shall use. So we are going to need to develop the theory of quaternionic modular forms, which is rather different to the theory of classical modular forms (for example, in the cases we need, the definition is completely algebraic; there are no holomorphic functions in sight, and the analogue of the upper half plane in the quaternionic theory is a finite set of points).

We could just launch into the general theory over totally real fields, which will be the generality which we'll need. But when I was a PhD student, I learnt about these objects by playing with explicit examples. So, whilst not logically necessary for the proof, I thought it would be fun, and perhaps also instructional, to compute a concrete example of a space of quaternionic modular forms. The process of constructing the example might even inform what kind of machinery we should be developing in general. Let's begin by discussing the quaternion algebra we shall use.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.