5.1. 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 \SL_2(\R) and \SL_2(\Z) are intimately involved; these are the norm 1 units in the matrix rings M_2(\R) and M_2(\Z). In the theory of quaternionic modular forms, the analogous groups are the norm 1 units in rings such as Hamilton's quaternions \R\oplus\R i\oplus\R j\oplus\R k, and subrings such as \Z\oplus\Z i\oplus\Z j\oplus\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.

5.2. A quaternion algebra🔗

Let's define D to be the quaternion algebra \Q\oplus\Q i\oplus\Q j\oplus\Q k. As a vector space, D is 4-dimensional over \Q with [1,i,j,k] giving a basis. It has a (non-commutative) ring structure, with multiplication satisfying the usual quaternion algebra relations i^2=j^2=k^2=ijk=-1. You can think of D as an analogue of 2 × 2 matrices with rational coefficients, hence its units D^\times are an analogue of the group \GL_2(\Q).

We will also need an analogue of the group \GL_2(\Z), which will come from an integral structure on D. We choose the Hurwitz order, namely the subring \calO:=\Z\oplus\Z i\oplus\Z j\oplus\Z \omega, where \omega=\frac{-1+(i+j+k)}{2}, a cube root of unity, as (i+j+k)^2=-3. The simplest way to understand \calO is that it's quaternions a+bi+cj+dk where either a,b,c,d are all integers or are all in \frac{1}{2}+\Z.

Note that \calO is a maximal order and a Euclidean domain, which is why we prefer it over the more obvious sublattice \Z\oplus\Z i\oplus\Z j\oplus\Z k.

In this chapter, we are going to compute a complex vector space which could be called something like the "weight 2 level 2 modular forms for D^\times". The main result will be that this space is 1-dimensional.

Note that mathlib has modular forms, but it doesn't have enough complex analysis to deduce that the space of modular forms of a given weight and level is finite-dimensional. If all the sorrys in this chapter are completed before mathlib gets the necessary complex analysis, then the first nonzero space of modular forms to be proved finite-dimensional in Lean will be a space of quaternionic modular forms.

We will use a modern "adelic" definition of our modular forms, so the first thing we need to do is to talk about profinite completions.

5.3. Zhat🔗

Classically automorphic forms were defined as functions on symmetric spaces (like the upper half plane) which transformed well under the action of certain discrete groups (for example \SL_2(\Z)). However such definitions became combinatorially problematic when generalised to number fields with nontrivial class group, because the classical theory needed a number p to define the Hecke operator T_p, and in the case where p was a non-principal prime ideal in a number field, there was no appropriate number. One fix is to take disjoint unions of symmetric spaces indexed by the ideal class group of the field in question, but it is easier to work adelically, which is morally what we shall do. However we are able to avoid introducing the adeles explicitly; we can work instead with the conceptually simpler object \Zhat, the profinite completion of \Z. So what is \Zhat? We offer a low-level definition of this object.

Note that it follows easily that that the map from the integers to \Zhat is injective.

But \Zhat is much larger than \Z; it has the same cardinality as the reals in fact. Let's write down an explicit example of an element of \Zhat which isn't obviously in \Z.

5.4. More Advanced Remarks On Zhat Versus Q🔗

This section can be skipped on first reading.

People who have seen some more advanced algebra might recognise this construction of \Zhat as being the profinite completion of the additive abelian group \Z, so it is a fundamental object of mathematics in some sense. But usually, when building mathematics, after \Z we go to \Q, a multiplicative localisation of \Z, and only complete after that (to get \R). The process of "completing before localising" gives us a far more arithmetic completion of \Z.

Even though \Q is a divisible abelian group and hence its profinite completion vanishes, we can still attempt to "locally profinitely complete it" by defining \Qhat:=\Q\otimes_{\Z}\Zhat. This object is more commonly known as the finite adeles of \Q. More generally if F is any number field then F\otimes_{\Z}\Zhat is the ring of finite adeles of F. To get to the full ring of adeles of a number field F you need to take the product with the ring of infinite adeles of F, which is F\otimes_{\Q}\R: some kind of universal archimedean completion of F. I don't know a reference which develops the theory of adeles in this way, so this is what we shall do here.

5.5. Qhat and tensor products.🔗

The definition of \Qhat is easy if you know about tensor products of additive abelian groups.

5.6. A crash course in tensor products🔗

We've defined \Qhat to be \Q\otimes\Zhat. Whatever does this mean? Well just to orient yourself, if A and B are additive abelian groups, then A\otimes B is also an abelian group. And if A and B are commutative rings (as they are in our case), then A\otimes B is also a commutative ring.

Even if A and B are completely concrete commutative rings, their tensor product A\otimes B might be incomprehensible. For example \bbC\otimes\bbC is completely incomprehensible (note that we are tensoring over the integers). It is not like the product of groups or the disjoint union of two sets, where you have a completely explicit unambiguous formula for each element.

In this sense, the theory of tensor products is a bit like the theory of continuous functions. Humanity started off studying concrete polynomial equations such as x^2+1 and then moved on to concrete analytic functions such as \log(x) and \sin(x), but eventually the abstract concept of a continuous function from the reals to the reals was born. There is no "formula" for a general continuous function, and continuous functions such as e^{-1/x^2} or |x| have no power series. Even if there were a formula for a specific continuous function of interest, it is not clear in general how to make sense of the claim that it's the "best" formula. In other words, there is no "canonical form" for a general continuous function, and yet we prove things about them anyway. We shall adopt the same attitude for elements of A\otimes B.

The first thing to know about the tensor product A\otimes B of two abelian groups A and B is a "constructor" for the type. In other words, how can we make elements A\otimes B? Well, it turns out that given elements a\in A and b\in B, we can form the element a\otimes_t b\in A\otimes B.

Recall that the sum of all the factorials is an element e\in\Zhat, and 22/7 is certainly a rational number, so we can make the element \frac{22}{7}\otimes_te\in\Qhat.

This example is in the Lean code.

Elements of the form a\otimes_t b\in A\otimes B are known as pure tensors. In the literature, pure tensors are often written a\otimes b, but we shall follow mathlib's convention in reserving the \otimes symbol for groups like A \otimes B, and adorning it with a t when using it on elements of the groups (or, as Lean calls them, terms, which explains the notation).

Addition of pure tensors obeys the "distributivity" rules a\otimes_t b_1+a\otimes_t b_2=a\otimes_t(b_1+b_2) and a_1\otimes_t b+a_2\otimes_t b=(a_1+a_2)\otimes_t b, but there is no rule which simplifies a general sum a\otimes_t b + c\otimes_t d into a pure tensor. Indeed, in general it is not the case that every element of a tensor product A\otimes B is of the form a\otimes_t b; there can be tensors which aren't pure. However every element of A\otimes B is a finite sum of pure tensors, with the result that one can attempt to define additive maps from A\otimes B by saying what they do on pure tensors, and then extending linearly.

Another thing worth understanding is that just like how rational numbers can be written as quotients of integers in several ways (for example 1/2=2/4=3/6=\cdots), a general pure tensor in A\otimes B can be represented as a\otimes_t b in many ways. For example, in \Qhat we have 1\otimes_t 2=2\otimes_t 1. A general rule for equality of pure tensors is that if a\in A and b\in B and z\in\Z, then za\otimes_tb=a\otimes_tzb; integers can move over the tensor symbol. But equality is hard: in general there may not be an algorithm to decide whether two pure tensors a\otimes_t b and c\otimes_t d are equal in A\otimes B.

A summary of the situation: if A and B are abelian groups, then every element of A\otimes B can be written in the form \sum_{i=1}^Na_i\otimes_tb_i. It's just that this representation is highly nonunique, and furthermore given explicit elements a_1,a_2\in A and b_1,b_2\in B it might be a hard problem to figure out if a_1\otimes_t b_1=a_2\otimes_t b_2.

For example, it turns out that (\Z/2\Z)\otimes(\Z/3\Z)=0 and so in this tensor product all the a\otimes_t b are equal to each other and to 0\otimes 0.

Having said all of that, one nice property of \Qhat is that every tensor is pure; let's prove this now.

Be careful though: just because every element of \Qhat can be written as q\otimes z, this representation may not be unique. For example 2\otimes 1=1\otimes 2. However, writing \frac{1}{N}\otimes_t z as z/N does tempt us into the following definition.

If A and B are additive abelian groups then A\otimes B is also an additive abelian group. However if A and B are commutative rings, then A\otimes B also inherits the structure of a commutative ring, with 0=0\otimes_t 0 and 1=1\otimes_t 1. Pure tensors multiply in the obvious way: the product of a_1\otimes_t b_1 and a_2\otimes_t b_2 is a_1a_2\otimes_t b_1b_2. There are ring homomorphisms A\to A\otimes B and B\to A\otimes B sending a to a\otimes_t 1 and b to 1\otimes_t b. In general such maps are not injective, but in the case of \Qhat=\Q\otimes\Zhat both maps from \Q and \Zhat are inclusions.

5.7. Additive structure of Qhat.🔗

Here we forget the ring structure on everything, and analyse \Qhat as an additive abelian group, and in particular how the subgroups \Z, \Q and \Zhat sit within it.

The two results we prove in this section are that \Q\cap\Zhat=\Z and that \Q+\Zhat=\Qhat. Using lattice-theoretic notation we could write these results as \Q\sqcap\Zhat=\Z and \Q\sqcup\Zhat=\Qhat.

5.8. Multiplicative structure of the units of Qhat.🔗

We now forget the additive structure on the commutative ring \Qhat and consider the multiplicative structure of its group of units \Qhat^\times (which I couldn't get into the section title). We have the obvious subgroups \Q^\times, \Z^\times and \Zhat^\times.

Note that by the previous lemma, this representation will be unique up to sign.

5.9. The Hurwitz quaternions🔗

This ring is isomorphic to \Z^4 as an additive group, and \calO\otimes_{\Z}\R=\R\oplus \R i\oplus \R j\oplus\R \omega is the usual Hamilton quaternions.