8 Appendix: A collection of results which are needed in the proof.
In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
8.1 Results from class field theory
We start with the local case. In fact we restrict to the \(p\)-adic case, but only for simplicity of exposition because it’s all we’ll need (and, to be frank, because I’m not 100 percent of what is true in the function field case).
Let \(K\) be a finite extension of \(\mathbb {Q}_p\). We write \(\widehat{\mathbb {Z}}\) for the profinite completion of \(\mathbb {Z}\); it is isomorphic to \(\prod _p\mathbb {Z}_p\) where \(\mathbb {Z}_p\) is the \(p\)-adic integers and the product is over all primes.
The maximal unramified extension \(K^{un}\) in a given algebraic closure of \(K\) is Galois over \(K\) with Galois group “canonically” isomorphic to \(\widehat{\mathbb {Z}}\) in two ways; one of these two isomorphisms identifies \(1\in \widehat{\mathbb {Z}}\) with an arithmetic Frobenius (the endomorphism inducing \(x\mapsto x^q\) on the residue field of \(K^{un}\), where \(q\) is the size of the residue field of \(K\)). The other identifies 1 with geometric Frobenius (defined to be the inverse of arithmetic Frobenius).
It is impossible to say which of the two canonical isomorphisms is “the most canonical”; people working in different areas make different choices in order to locally minimise the number of minus signs in their results.
As a result, the absolute Galois group of \(K\) surjects onto \(\widehat{\mathbb {Z}}\); its kernel is said to be the inertia subgroup of this Galois group. Now pull back this surjection along the continuous map from \(\mathbb {Z}\) (with its discrete topology) to \(\widehat{\mathbb {Z}}\), in the category of topological groups. We end up with a group containing the inertia group as an open normal subgroup, and with quotient isomorphic to the integers.
The topological group described above is called the Weil group of \(K\).
The following theorem is nontrivial.
If \(K\) is a finite extension of \(\mathbb {Q}_p\) then there are two “canonical” isomorphisms of topological abelian groups, between \(K^\times \) and the abelianisation of the Weil group of \(K\).
This is the main theorem of local class field theory; see for example the relevant articles in [ 4 ] or many other places.
Note that María Inés de Frutos Fernández and Filippo Nuccio are working on a formalisation of the proof of this using Lubin–Tate formal groups.
Now let \(M\) be an abelian group (with the discrete topology) equipped with a continuous action of \(G_K\), the Galois group \(\operatorname{Gal}(K^{\operatorname{sep}}/K)\) where we fix an algebraic closure \(\overline{K}\) of \(K\). Note that if one doesn’t want to choose an algebraic closure of \(K\) one can instead think of \(M\) as being an etale sheaf of abelian groups on \(\operatorname{Spec}(K)\).
Continuous group cohomology \(H^i(G_K,M)\) in this setting can be defined using continuous cocycles and continuous coboundaries, or just as a colimit of usual group cohomology over the finite quotients of this absolute Galois group (or as etale cohomology, if you prefer). Here are some of the facts we will need about cohomology in this situation. A nice summary is that cohomology of a local Galois group behaves like the cohomology of a compact connected 2-manifold. All the theorems below will need extensive planning.
If \(M\) is finite then the cohomology groups \(H^i(G_K,M)\) all finite.
This is Proposition 14 in section 5.2 of [ 12 ] .
If \(M\) is torsion then \(H^i(G_K,M)=0\) if \(i{\gt}2\).
This follows from Proposition 15 in section 5.3 of [ 12 ] .
\(H^2(G_K,\mu _n)\) is “canonically” isomorphic to \(\mathbb {Z}/n\mathbb {Z}\).
This is also included in Lemma 2 of section 5.2 of [ 12 ] (Serre just writes that the groups are equal; he clearly is not a Lean user. I can see no explanation in his book of this use of the equality symbol. When the statement of this “theorem” is formalised in Lean it may well actually be a definition, giving the map).
If \(\mu =\bigcup _{n\geq 1}\mu _n\) and \(M':=\operatorname{Hom}(M,\mu )\) is the dual of \(M\) then for \(0\leq i\leq 2\) the cup product pairing \(H^i(G_K,M)\times H^{2-i}(G_K,M')\to H^2(G_K,\mu )=\mathbb {Q}/\mathbb {Z}\) is perfect.
This is Theorem 2 in section 5.2 in [ 12 ] . Note again the dubious (as far as Lean is concerned) use of the equality symbol.
If \(h^i(M)\) denotes the order of \(H^i(G_K,M)\) then \(h^0(M)-h^1(M)+h^2(M)=0\).
If \(\mu _\infty \) denotes the Galois module of all roots of unity in our fixed \(\overline{K}\), then one can define the dual Galois module \(M'\) as \(\operatorname{Hom}(M,\mu )\) with its obvious Galois action.
If \(0\leq i\leq 2\) then the cup product gives us a map \(H^i(K,M)\times H^{2-i}(K,M')\to H^2(K,\mu _\infty )\).
(i) There is a “canonical” isomorphism \(H^2(K,\mu _\infty )=\mathbb {Q}/\mathbb {Z}\); (ii) The pairing above is perfect.
This is Theorem II.5.2 in [ 12 ] .
We now move onto the global case. If \(N\) is a number field, that is, a finite extension of \(\mathbb {Q}\), then let \(\mathbb {A}_N^f:= N\otimes _{\mathbb {Z}}\widehat{\mathbb {Z}}\) denote the finite adeles of \(N\) and let \(N_\infty := N\otimes _{\mathbb {Q}}\mathbb {R}\) denote the product of the completions of \(N\) at the infinite places, so \(\mathbb {A}_N:=\mathbb {A}_N^f\times N_\infty \) is the ring of adeles of \(N\).
If \(N\) is a finite extension of \(\mathbb {Q}\) then there are two “canonical” isomorphisms of topological groups between the profinite abelian groups \(\pi _0(\mathbb {A}_N^\times /N^\times )\) and \(\operatorname{Gal}(\overline{N}/N)^{\operatorname{ab}}\); one sends local uniformisers to arithmetic Frobenii and the other to geometric Frobenii; each of the global isomorphisms is compatible with the local isomorphisms above.
This is the main theorem of global class field theory; see for example Tate’s article in [ 4 ] .
We need the following consequence:
Let \(S\) be a finite set of places of a number field \(K\) . For each \(v \in S\) let \(L_v/K_v\) be a finite Galois extension. Then there is a finite solvable Galois extension \(L/K\) such that if \(w\) is a place of \(L\) dividing \(v \in S\), then \(L_w/K_v\) is isomorphic to \(L_v/K_v\) as \(K_v\)-algebra. Moreover, if \(K^{\operatorname{avoid}} /K\) is any finite extension then we can choose \(L\) to be linearly disjoint from \(K^{\operatorname{avoid}}\).
We also need Poitou-Tate duality; I’ll refrain from writing it down for now, because we don’t even have Galois cohomology in Lean yet (although we are very close to it).
8.2 Structures on the points of an affine variety.
All rings and algebras in this section are commutative with a 1, and all morphisms send 1 to 1.
Let \(X=\operatorname{Spec}(A)\) be an affine scheme of finite type over a field \(K\). For example \(X\) could be an affine algebraic variety; in fact we shall only be interested in smooth affine varieties in the applications, but the initial definition and theorem are fine for all finite type schemes.
If \(R\) is any \(K\)-algebra then one can talk about the \(R\)-points \(X(R)\) of \(X\), which in this case naturally bijects with the \(K\)-algebra homomorphisms from \(A\) to \(R\).
If \(X\) is an affine scheme of finite type over \(K\), and if \(R\) is a \(K\)-algebra which is also a topological ring, then we define a topology on the \(R\)-points \(X(R)\) of \(K\) by embedding the \(K\)-algebra homomorphisms from \(A\) to \(R\) into the set-theoretic maps from \(A\) to \(R\) with its product topology, and giving it the subspace topology.
If \(X\) is as above and \(X\to \mathbb {A}^n_K\) is a closed immersion, then the induced map from \(X(R)\) with its topology as above to \(R^n\) is an embedding of topological spaces (that is, a homeomorphism onto its image).
See Conrad’s notes.
We now specialise to the smooth case. I want to make the following conjectural “definition”:
Let \(K\) be a field equipped with an isomorphism to the reals, complexes, or a finite extension of the \(p\)-adic numbers. Let \(X\) be a smooth affine algebraic variety over \(K\). Then the points \(X(K)\) naturally inherit the structure of a manifold over \(K\).
Probably this is fine for a broader class of fields \(K\).
If \(X\) is as in the previous definition and \(X\to \mathbb {A}^n_K\) is a closed immersion, then the induced map from \(X(K)\) with its manifold structure to \(K^n\) is an embedding of manifolds.
I’m assuming this is standard, if true.
If \(G\) is an affine algebraic group of finite type over \(K=\mathbb {R}\) or \(\mathbb {C}\) then \(G(K)\) is naturally a real or complex Lie group.
The corollary, for sure, is true! And it’s all we need. I have not yet made any serious effort to find a reference for the definition or independence, although there seem to be some ideas here. As a toy example, one can embed \(\operatorname{GL}_n(\mathbb {R})\) into either \(\mathbb {R}^{n^2+1}\) via \(M\mapsto (M,\det (M)^{-1})\) or into \(\mathbb {R}^{2n^2}\) via \(M\mapsto (M,M^{-1})\) and the claim is that the two induced manifold structures are the same.
8.3 Algebraic groups.
The concept of an affine algebraic group over a field \(K\) can be implemented in Lean as a commutative Hopf algebra over \(K\), as a group object in the category of affine schemes over \(K\), as a representable group functor on the category of affine schemes over \(K\), or as a representable group functor on the category of schemes over \(K\) which is represented by an affine scheme. All of these are the same to mathematicians but different to Lean and some thought should go into which of these should be the actual definition, and which should be proved to be the same thing as the definition.
An affine algebraic group \(G\) of finite type over a field \(k\) is said to be connected if it is connected as a scheme, and reductive if \(G_{\overline{k}}\) has no nontrivial smooth connected unipotent normal \(k\)-subgroup.
8.4 Automorphic forms and representations
This section needs a lot of work; I am just attempting to write down some approximation to the (well-known) definitions but in great generality (far greater than we need). Some definitions below are short on details; indeed there may even be errors or imprecisions right now (because we are working in more generality than I am used to). It will be a very interesting project to get these details down. One reference (which leaves a lot of exercises) is Borel-Casselman in [ 2 ] . Even stating these definitions will be a big challenge in Lean; indeed one of the motivations of the project is that it forces us to write down all the below properly.
Let \(G\) be a connected reductive group over a number field \(N\). We note that \(G(\mathbb {A}_N^f)\) is a (locally profinite) topological space and \(G(N_\infty )\) is a real Lie group; their product is \(G(\mathbb {A}_N)\). If \(g\in G(\mathbb {A}_N)\), write \(g_f\in G(\mathbb {A}_N^f)\) for the finite part and \(g_\infty \in G(N_\infty )\) for its infinite part.
For some reason, in the literature people seem to fix a choice of maximal compact subgroup \(U_\infty \) of \(G(N_\infty )\). I believe that all such subgroups are conjugate, and probably this gives some route between the different definitions coming from the different choices.
Example: if \(G=\operatorname{GL}_2\) and \(N=\mathbb {Q}\) then \(N_\infty =\mathbb {R}\) and \(G(N_\infty )\) is just \(\operatorname{GL}_2(\mathbb {R})\) with its usual Lie group structure and we can take \(U_\infty \) to be \(O_2(\mathbb {R})\); \(G(\mathbb {A}_N^f)\) is the restricted product of \(\operatorname{GL}_2(\mathbb {Q}_p)\) over \(\operatorname{GL}_2(\mathbb {Z}_p)\), for all primes \(p\).
By assumption, \(G(N_\infty )\) admits a finite-dimensional (algebraic) representation \(\rho \) with finite kernel. Consider \(\rho \) as taking values in \(GL_N(\mathbb {C})=\operatorname{Aut}_{\mathbb {C}}(V)\). Fix a hermitian sesquilinear form on \(V\) which is \(U_\infty \) invariant, and now define a norm \(||g||_\rho \) on \(G(N_\infty )\) by
where the asterisk denotes adjoint with respect to the sesquilinear form. According to the article by Borel–Jacquet in [ 2 ] (p189), if \(\rho '\) is another such choice then there exists a positive real \(C\) and a positive integer \(n\) such that \(||g||_{\rho '}\leq C||g||_\rho ^n\) for all \(g\in G(N_\infty )\).
A function \(f : G(N_\infty )\to \mathbb {C}\) is slowly-increasing if there exists some \(C{\gt}0\) and \(n\geq 1\) such that \(|f(x)\leq C||x||_\rho ^n\).
This is independent of the choice of \(\rho \) as above.
Follows from the above.
We can now give the definition of an automorphic form. For FLT we only need the definition for \(G\) being either an abelian algebraic group, or an inner form of \(GL(2)\), but we have chosen to work in full generality here.
An automorphic form is a function \(\phi :G(\mathbb {A}_N)\to \mathbb {C}\) satisfying the following conditions:
\(\phi \) is locally constant on \(G(\mathbb {A}_N^f)\) and \(C^\infty \) on \(G(N_\infty )\). In other words, for every \(g_\infty \), \(\phi (-,g_\infty )\) is locally constant, and for every \(g_f\), \(\phi (g_f,-)\) is smooth.
\(\phi \) is left-invariant under \(G(N)\);
\(\phi \) is right-\(U_\infty \)-finite (that is, the space spanned by \(x\mapsto \phi (xu)\) as \(u\) varies over \(U_\infty \) is finite-dimensional);
\(\phi \) is right \(K_f\)-finite, where \(K_f\) is one (or equivalently all) compact open subgroups of \(G(\mathbb {A}_N^f)\);
\(\phi \) is \(\mathcal{z}\)-finite, where \(\mathcal{z}\) is the centre of the universal enveloping algebra of the Lie algebra of \(G(N_\infty )\), acting via differential operators. Equivalently \(\phi \) is annihiliated by a finite index ideal of this centre, so morally \(\phi \) satisfies lots of differential equations of a certain type;
For all \(g_f\), the function \(g_\infty \mapsto \phi (g_f g\infty )\) is slowly-increasing in the sense above.
Automorphic forms form a typically infinite-dimensional vector space.
An automorphic form is cuspidal (or “a cusp form”) if it furthermore satisfies \(\int _{U(N)\backslash U(\mathbb {A}_N)}\phi (ux)du=0\), where \(P\) runs through all the proper parabolic subgroups of \(G\) defined over \(N\) and \(U\) is the unipotent radical of \(P\), and the integral is with respect to the measure coming from Haar measure.
The cuspidal automorphic forms form a complex subspace of the space of automorphic forms.
The group \(G(\mathbb {A}_N)\) acts on itself on the right, and this induces a left action of its subgroup \(G(\mathbb {A}_N^f)\times U_\infty \) on the spaces of automorphic forms and cusp forms. The Lie algebra \(\mathfrak {g}\) of \(G(N_\infty )\) also acts, via differential operators. Furthermore the actions of \(\mathfrak {g}\) and \(U_\infty \) are compatible in the sense that the differential of the \(U_\infty \) action is the action of its Lie algebra considered as a subalgebra of \(\mathfrak {g}\). We say that the spaces are \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\)-modules.
The cusp forms decompose as a (typically infinite) direct sum of irreducible \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\)-modules.
A cuspidal automorphic representation is an irreducible \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\)-module isomorphic to an irreducible summand of the space of cusp forms.
For non-cuspidal representations, they do not decompose as a direct sum; there is a continuous spectrum which decomposes as a direct integral. We may not ever need these. As a result the definition of an automorphic representation has to be slightly modified in the non-cuspidal case.
An automorphic representation is an irreducible \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\)-module isomorphic to an irreducible subquotient of the space of automorphic forms.
Admissibility is a finiteness condition on an irreducible representation of \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\); automorphic representations are admissible, and this seems to boil down to theorems of Godement and Harish-Chandra in the general case.
An irreducible admissible \((G(\mathbb {A}_N^f)\times U_\infty ,\mathfrak {g})\)-module is a restricted tensor product of irreducible representations \(\pi _v\) of \(G(N_v)\) as \(v\) runs through the finite places of \(N\), tensored with a tensor product of irreducible \((\mathfrak {g}_v,U_{\infty ,v})\)-modules as \(v\) runs through the infinite places of \(N\). The representations \(\pi _v\) are unramified for all but finitely many \(v\).
See Flath’s article in [ 3 ] .
As mentioned above, we only need all of this for abelian algebraic groups and for inner forms of \(\operatorname{GL}_2\) over totally real fields, where everything can be made more concrete (and in particular where I can write down concrete definitions, although this still needs to be done). In particular, we don’t strictly speaking need all of the above, we could just cheat and deal with \(\operatorname{GL}_2(\mathbb {R})\) and \(\mathbb {H}^\times \) separately.
The theorems I need are: Jacquet-Langlands for inner forms of \(\operatorname{GL}_2\) over totally real fields, and multiplicity 1 for these inner forms. We also need cyclic base change plus classification of image, all for totally definite quaternion algebras, and we need automorphic induction from \(\operatorname{GL}_1(K)\) to \(\operatorname{GL}_2(F)\) when \(K/F\) is a degree 2 totally imaginary extension. There seems to be little point formalising the statements of the theorems if we cannot yet even formalise the definition of an automorphic representation properly.
8.5 Galois representations
Ivan Farabella has formalised the definition of a compatible family of Galois representations, modulo the existence of Frobenius elements, which has been established by Jou Glasheen.
Let \(N\) be a number field. A compatible family of \(d\)-dimensional Galois representations over \(N\) is a finite set of finite places \(S\) of \(N\), a number field \(E\), a monic degree \(d\) polynomial \(F_{{\mathfrak {p}}}(X)\in E[X]\) for each finite place \({\mathfrak {p}}\) of \(K\) not in \(S\) and, for each prime number \(\ell \) and field embedding \(\phi : E\to \overline{\mathbb {Q}}_\ell \) (or essentially equivalently for each finite place of \(E\)), a continuous homomorphism \(\rho :\operatorname{Gal}(K^{\operatorname{sep}}/K)\to \operatorname{GL}_2(\overline{\mathbb {Q}}_\ell )\) unramified outside \(S\) and the primes of \(K\) above \(\ell \), such that \(\rho (\operatorname{Frob}_{\mathfrak {p}})\) has characteristic polynomial \(P_\pi (X)\) if \(\pi \) lies above a prime number \(p\not=\ell \) with \(p\not\in S\).
The big theorem, which again we are far from even stating right now, is
Given an automorphic representation \(\pi \) for an inner form of \(\operatorname{GL}_2\) over a totally real field and with reflex field \(E\), such that \(\pi \) is weight 2 discrete series at every infinite place, there exists a compatible family of 2-dimensional Galois representations associated to \(\pi \), with \(S\) being the places at which \(\pi \) is ramified, and \(F_{{\mathfrak {p}}}(X)\) being the monic polynomial with roots the two Satake parameters for \(\pi \) at \({\mathfrak {p}}\).
8.6 Algebraic geometry
We have already mentioned Mazur’s Theorem on torsion subgroups of elliptic curves (theorem 3.27). The proof of this is the main theorem of [ 9 ] , 150 pages of subtle arithmetic geometry involving the bad reduction of modular curves, exotic cohomology theories (etale and more), and the consequences of this for the Neron models of their Jacobians. After a beautiful introductory chapter containing a history and examples, the convention is established that throughout the paper, \(N\) will denote a prime number which is at least 5. And then the first sentence of chapter 1 of the paper proper is “Consider quasi-finite separated commutative group schemes of finite presentation over the base \(S:=\operatorname{Spec}{\mathbb {Z}}\) which are finite flat group schemes over \(S':=\operatorname{Spec}(Z[1/N]).\)”. At the time of writing (May 2024), Lean’s algebraic geometry cannot get us through the first sentence of Mazur’s proof, which occupies pages 43 to 172 of the paper (not including the appendix or references, that’s just the proof). Anyone interested in formalising Mazur’s paper should make a formalisation of its first sentence their first milestone.
Talking of modular curves, we also need the existence of Shimura curves and surfaces over totally real fields \(F\) (of degree greater than 2, so always compact). The curves are "modeles étranges" in the sense of Deligne, so we also need moduli spaces of unitary Shimura varieties over CM extensions. We need to decompose the first and second etale cohomology groups of these varieties into Galois representations, by understanding them in terms of automorphic representations.
We need the definition of (the canonical model over \(F\) of) the Shimura curve attached to an inner form of \(\operatorname{GL}_2\) with precisely one split infinite place, and the same for the Shimura surface associated to an inner form split at two infinite places (and ramified elsewhere, so it’s compact).
We also need Moret-Bailly’s theorem from [ 10 ] :
Let \(K^{\operatorname{avoid}}/K\) be a Galois extension of number fields. Suppose also that \(S\) is a finite set of places of \(K\). For \(v\in S\) let \(L_v/K_v\) be a finite Galois extension. Suppose also that \(T /K\) is a smooth, geometrically connected curve and that for each \(v\in S\) we are given a nonempty, \(\operatorname{Gal}(L_v/K_v)\)-invariant, open subset \(\Omega _v\subseteq (L_v)\). Then there is a finite Galois extension \(L/K\) and a point \(P ∈ T (L)\) such that
\(L/K\) is Galois and linearly disjoint from \(K^{\operatorname{avoid}}\) over \(K\);
if \(v\in S\) and \(w\) is a prime of \(L\) above \(v\) then \(L_w /K_v\) is isomorphic to \(L_v/K_v\);
and \(P \in \Omega _v\subseteq T (L_v) \cong (L_w)\) via one such \(K_v\)-algebra morphism (this makes sense as \(\Omega _v\) is \(\operatorname{Gal}(L_v/K v)\)-invariant).
Note that we do not even have the definition of a curve over a field in Lean.
8.7 Algebra
We need the classification of finite subgroups of \(\operatorname{PGL}_2(\overline{\mathbb {F}}_p)\). The answer is that they are all cyclic, dihedral, \(A_4\), \(S_4\), \(A_5\), or isomorphic to \(\operatorname{PSL}_2(k)\) or \(\operatorname{PGL}_2(k)\) for some finite field of characteristic \(p\). This should at least be easy to state!