13.1. Status🔗

This is an active miniproject. The abstract theory is completely formalized; at the time of writing the concrete theory has no sorried definitions but it does have some sorried proofs.

13.2. Goal🔗

The goal of this project is to get sorry-free definitions of Hecke operators acting on spaces of automorphic forms. These Hecke operators generate Hecke algebras, which are the rings called T in the modularity lifting theorems, or R=T theorems, crucially introduced by Wiles in order to prove FLT.

The theory comes in two parts; the "abstract" theory, which is pure algebra, and the "concrete" theory where we apply the abstract constructions to produce endomorphisms of spaces of automorphic forms. The abstract theory is short (and completely formalized); the concrete theory still needs some work because to apply the theory to the adelic groups we care about we need to develop some more API around the theory of restricted products, and of compact open subgroups of matrix groups.

13.3. Abstract theory🔗

The set-up: we have a commutative ring $R$, the coefficient ring, and all of our spaces which the operators act on will be $R$-modules.

We have a group G acting R-linearly on an R-module A.

We have subgroups U and V of G. We will be particularly interested in the R-modules A^U and A^V of invariant elements.

Given an element g \in G, then under a certain finiteness hypothesis we will be able to define an R-linear map T_g or [UgV] from A^V to A^U. The finiteness hypothesis is that the double coset UgV can be written as a finite union of single cosets g_iV.

The finiteness hypothesis that the decomposition UgV = \coprod_i g_iV is into a finite union is necessary for the theory to work. If G is a topological group then here is a criterion which gives the finiteness hypothesis for free.

13.4. Restricted products🔗

In the concrete example of Hecke operators which we care about, the invariants A^G will be spaces of quaternionic automorphic forms by definition. We do not need to worry about the definition of A in this project at all. However we will need to do various computations with the specific groups G which we are interested in, and they are restricted products. So we now develop some theory for restricted products, starting by recalling the definition.

If I is an index set, if X_i are sets indexed by i\in I and if Y_i are subsets, then the restricted product \prod'_iX_i is defined to be the subset of the full product \prod_i X_i consisting of those tuples (x_i) such that x_i\in Y_i for all but finitely many i. We suppress the Y_i from the notation in this document, although in Lean we cannot do this and the restricted product looks something like \prod{}^{r} i,[X\ i, Y\ i].

It is straightforward to check that if the X_i are groups or rings or R-modules, and the Y_i are subgroups or subrings or submodules, then the restricted product is a group, ring or R-module. Indeed the structure is inherited via the inclusion \prod'_iX_i\subseteq\prod_iX_i and the fact that arbitrary products of groups, rings, and modules are groups, rings, and modules.

More subtle is the theory of topological space structures. If the X_i are topological spaces then we do not give \prod'_iX_i the subspace topology coming from the product topology on \prod_iX_i; instead we give it the finest topology making all of the natural maps \prod_{i\in S}X_i\times\prod_{i\notin S}Y_i\to \prod'_iX_i continuous, as S runs through all finite subsets of I. Here the product of X_is and Y_is has the product topology. For example if all of the Y_i are open then one can check that \prod_iY_i is an open subset of \prod'_iX_i, whereas it is not of the form \left(\prod'_iX_i\right)\cap U for any open subset U of \prod_iX_i in general; the map from \prod'_iX_i to \prod_iX_i is continuous but is not in general an embedding.

If you have seen automorphic forms before, then here is an obvious-sounding claim: because the adeles \mathbb{A}_F of a number field are a restricted product of completions F_v with respect to the integer rings \mathcal{O}_v, then GL_2(\mathbb{A}_F) is obviously topologically a restricted product of GL_2(F_v) with respect to GL_2(\mathcal{O}_v). We now spend some time justifying this claim, which is a little more intricate than it sounds.

This may well not be true if B_i and D_i are not open, because filtered colimits and binary products do not appear in general to commute in the category of topological spaces. I don't know an explicit counterexample though.

M^\times does not get the subspace topology from M; it is embedded into M \times M via g \mapsto (g, g^{-1}) and gets the subspace topology from the product. This makes it into a topological group.

Is Hausdorffness necessary?

We could work over a general nonarchimedean normed field but we still do not have them in mathlib, so we stick to the case of interest which is the completion of a number field K at a finite place v. Such a completion is a topological field K_v equipped with a discrete valuation, a ring of integers \calO_v having a principal maximal ideal (\varpi), and a finite residue field k_v := \calO_v/(\varpi).

There is no formal Lean code for the lemmas in this section; it would seem more sensible to prove them in the right generality, and we don't have a definition of nonarchimedean local field yet.

13.5. Some local theory🔗

Recall that there is a projection \calO_v \to k_v where k_v is the residue field of v, a finite field. This induces a ring homomorphism M_2(\calO_v) \to M_2(k_v) with kernel M_2(\varpi\calO_v), an ideal I of M_2(\calO_v) isomorphic to (\varpi\calO_v)^4 and hence also compact and open.

Say \Gamma_v is a subgroup of GL_2(k_v). Then \Gamma_v is finite. Consider it as a submonoid of the multiplicative monoid M_2(k_v). Its preimage U_v in M_2(\calO_v) is easily checked to be a submonoid of M_2(\calO_v); furthermore it is a finite union of cosets of I and is hence compact and open as a submonoid of M_2(\calO_v) and hence of M_2(K_v).

Say now \begin{pmatrix}1&*\\0&1\end{pmatrix}\subseteq\Gamma_v\subseteq\begin{pmatrix}*&*\\0&*\end{pmatrix} and let U:=U_v be its preimage in GL_2(\calO_v), considered as a compact open subgroup of GL_2(K_v). Choose 0\not=\alpha\in\calO_v and define g=\begin{pmatrix}\alpha&0\\0&1\end{pmatrix}\in GL_2(K_v). Let's do an explicit double coset decomposition in preparation for a calculation with Hecke operators.

13.6. Adelic groups🔗

We are finally ready to discuss the group G and the subgroups U which we will be using to define our Hecke operators. Let K be a number field, let D a quaternion algebra over K and let A_K^\infty be the finite adeles of K; recall that this is a commutative topological ring, defined to be the restricted product of the commutative topological fields K_v as v runs through the finite places of K, with respect to the compact open subrings \calO_v.

The group~$G$ we are interested in for the rest of this miniproject is the group $(DotimesKAK^infty)^times$. We want to write down compact open subgroups of this group, but the first thing we need to do is to find a way of talking about elements of the group.

We will assume that there exists an \A_K^\infty-algebra isomorphism D\otimes_K\A_K^\infty=M_2(\A_K^\infty) and we will fix such an isomorphism r, called a rigidification in the Lean code. We give both of these \A_K^\infty-algebras the \A_K^\infty-module topology, which is a fancy way of saying the product topology. They are both free of rank 4 as \A_K^\infty-modules, and the rigidification is then a homeomorphism because all \A_K^\infty-module maps between modules with the \A_K^\infty-module topology are continuous.

This means that our group~$G$ is isomorphic (both algebraically and topologically) to $GL2(AK^infty)$. Before we go any further, let say something about matrix rings over complete fields.