You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardexpand all lines: blueprint/src/chapter/ch05bestiary.tex
+118-19
Original file line number
Diff line number
Diff line change
@@ -2,6 +2,60 @@ \chapter{A collection of results which are needed in the proof.}
2
2
3
3
In this (temporary) chapter 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 multi-year research projects. The purpose of this chapter right now is to give the community some kind of idea of the task we face.
4
4
5
+
\section{Results from class field theory}
6
+
7
+
We start with the local case.
8
+
9
+
Let $K$ be a finite extension of $\Q_p$. We write $\widehat{Z}$ for the profinite completion of $\Z$;
10
+
it is isomorphic to $\prod_p\Z_p$ where $\Z_p$ is the $p$-adic integers.
11
+
12
+
\begin{theorem}\label{maximal_unramified_extension_of_p-adic_field} The maximal unramified extension $K^{un}$ in a given algebraic closure of $K$
13
+
is Galois over $K$ with Galois group ``canonically'' isomorphic to $\widehat{Z}$ in two ways; one of these two canonical isomorphisms identifies $1\in\widehat{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 arithematic Frobenius).
14
+
\end{theorem}
15
+
16
+
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.
17
+
18
+
As a result, the absolute Galois group of $K$ surjects onto $\widehat{\Z}$; its kernel is said to be the \emph{inertia group} of this Galois group. Now pull back this surjection along the continuous map from $\Z$ (with its discrete topology) to $\widehat{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.
19
+
20
+
\begin{definition}\label{local_Weil_group} This topological group is called the \emph{Weil group} of $K$.
21
+
\end{definition}
22
+
23
+
\begin{theorem} If $K$ is a finite extension of $\Q_p$ then there are two ``canonical'' isomorphisms of topological abelian groups, between $K^\times$ the abelianisation of the Weil group of $K$.
24
+
\end{theorem}
25
+
\begin{proof} This is the main theorem of local class field theory; see for example~\cite{cf} (**TODO** more precise ref)
26
+
\end{proof}
27
+
28
+
Note that Maria Ines de Frutos Fernandez and Filippo Nuccio are working on a formalisation of the proof of this using Lubin-Tate formal groups.
29
+
30
+
Now let $M$ be a finite abelian group equipped with a continuous action of $G_K$, the Galois group $\GK$ where we fix an algebraic closure 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 $\Spec(K)$.
31
+
32
+
Continuous group cohomology 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). 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 $\Hom(M,\mu)$ with its obvious Galois action.
33
+
34
+
If $0\leq i\leq2$ then the cup product gives us a map $H^i(K,M)\times H^{2-i}(K,M')\to H^2(K,\mu_\infty)$.
35
+
36
+
\begin{theorem}[Local Tate duality]
37
+
(i) There is a ``canonical'' isomorphism $H^2(K,mu_\infty)=\Q/\Z$;
38
+
(ii) The pairing above is perfect.
39
+
\end{theorem}
40
+
\begin{proof}
41
+
This is Theorem II.5.2 in~\cite{serre-galcoh}.
42
+
\end{proof}
43
+
44
+
We now move onto the global case. If $N$ is a number field, that is, a finite extension of $\Q$,
45
+
then let $\A_N^f:= N\otimes_{\Z}\widehat{Z}$
46
+
denote the finite adeles of $N$ and let $N_\infty := N\otimes_\Q\R$ denote the product of the completions of $N$ at the infinite places, so $\A_N:=\A_N^f\times N_\infty$ is the ring of adeles of $N$.
47
+
48
+
\begin{theorem} If $N$ is a finite extension of $\Q$ then there are two ``canonical'' isomorphisms between the profinite abelian groups $\pi_0(\A_N^\times/N^\times)$ and $\GN^{\ab}$; one sends local uniformisers to arithemtic Frobenii and the other to geometric Frobenii; each of the global isomorphisms is compatible with the local isomorphisms above.
49
+
\end{theorem}
50
+
\begin{proof} This is the main theorem of global class field theory; see for example~\cite{cf} (**TODO** more precise ref).
51
+
\end{proof}
52
+
53
+
54
+
Existence of solvable extension avoiding a global extension and with prescribed local behaviour
55
+
56
+
Poitou-Tate
57
+
58
+
5
59
\section{Structures on the points of an affine variety.}
6
60
7
61
All rings and algebras in this section are commutative with a 1, and all morphisms send 1 to 1.
@@ -16,7 +70,7 @@ \section{Structures on the points of an affine variety.}
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 (that is, a homeomorphism onto its image).
73
+
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).
20
74
\end{theorem}
21
75
\begin{proof} See \href{https://math.stanford.edu/~conrad/papers/adelictop.pdf}{Conrad's notes}.
22
76
\end{proof}
@@ -30,19 +84,18 @@ \section{Structures on the points of an affine variety.}
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.
87
+
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.
If $G$ is an affine algebraic group of finite type over $K=\R$ or $\C$ then $G(K)$ is naturally a real or complex Lie group.
38
92
\begin{remark}
39
93
40
-
The corollary, for sure, is true! And it's all we need. I have not yet made any serious effort to find a reference.
94
+
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 \href{https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/top.20space.20.2F.20manifold.20structure.20on.20points.20of.20alg.20varieties/near/431812525}{here}.
41
95
42
96
\section{Algebraic groups.}
43
97
44
-
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
45
-
but different to Lean and some thought should go into which definition we use.
98
+
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.
46
99
47
100
\begin{definition}\label{connected_reductive_group} An affine algebraic group over a field of characteristic zero is said to be \emph{connected} if it is connected as a scheme, and \emph{reductive} if it admits a finite-dimensional semisimple representation with finite kernel.
48
101
\end{definition}
@@ -52,20 +105,73 @@ \section{Algebraic groups.}
52
105
53
106
\section{Automorphic forms and representations}
54
107
55
-
Let $G$ be a connected reductive group over a number field $N$. Let $\A_N^f:= N\otimes_{\Z}\widehat{Z}$
56
-
denote the finite adeles of $N$ and let $N_\infty := N\otimes_\Q\R$ denote the product of the completions of $N$ at the infinite places, so $\A_N:=\A_N^f\times N_\infty$ is the ring of adeles of $N$. We note
108
+
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 \cite{corvallis1}. Even \emph{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.
109
+
110
+
Let $G$ be a connected reductive group over a number field $N$. We note
57
111
that $G(\A_N^f)$ is a (locally profinite) topological space and $G(N_\infty)$ is a real Lie group;
58
-
their product is $G(\A_N)$.
112
+
their product is $G(\A_N)$. If $g\in G(\A_N)$, write $g_f\in G(\A_N^f)$ for the finite part and $g_\infty\in G(N_\infty)$ for its infinite part.
113
+
114
+
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.
59
115
60
-
We are at some points vague in the below definition, whose details are complex. For FLT
61
-
we only need the definition for $G$ being either an abelian algebraic group, or an inner
62
-
form of $GL(2)$. Furthermore, we seem to need to fix a choice of maximal compact subgroup
63
-
$U_\infty$ of $G(N_\infty)$.
116
+
Example: if $G=\GL_2$ and $N=\Q$ then $N_\infty=\R$ and $G(N_\infty)$ is just $\GL_2(\R)$ with its usual Lie group structure and we can take $U_\infty$ to be $O_2(\R)$; $G(\A_N^f)$ is the restricted product of $\GL_2(\Q_p)$ over $\GL_2(\Z_p)$, for all primes $p$.
117
+
118
+
By assumption, $G(N_\infty)$ admits a finite-dimensional (algebraic) representation $\rho$ with finite kernel. Consider $\rho$ as taking values in $GL_N(\C)=\Aut_\C(V)$. Fix a hermitian sesquilinear form on $V$ which
119
+
is $U_\infty$ invariant, and now define a norm $||g||_\rho$ on $G(N_\infty)$ by $$||g||_\rho=(\tr\rho(g)^*\rho(g))^{1/2}$$, where the asterisk denote adjoint with respect to the sesquilinear form. According to the article by Borel--Jacquet in \cite{corvallis1} (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)$.
120
+
121
+
\begin{definition} A function $f : G(N_\infty)\to\C$ is \emph{slowly-increasing} if there exists some $C>0$
122
+
and $n\geq1$ such that $|f(x)\leq C||x||_\rho^n$.
123
+
\end{definition}
124
+
125
+
\begin{theorem} This is independent of the choice of $\rho$ as above
126
+
\end{theorem}
127
+
\begin{proof} Follows from the above.
128
+
\end{proof}
129
+
130
+
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.
64
131
65
132
\begin{definition} An \emph{automorphic form} is a function $\phi:G(\A_N)\to\C$ satisfying the following conditions:
66
133
\begin{itemize}
134
+
\item$\phi$ is locally constant on $G(\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.
67
135
\item$\phi$ is left-invariant under $G(N)$;
136
+
\item$\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);
137
+
\item$\phi$ is right $K_f$-finite, where $K_f$ is one (or equivalentally all) compact open subgroups of $G(\A_N^f)$;
138
+
\item$\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;
139
+
\item For all $g_f$, the function $g_\infty\mapsto\phi(g_f g\infty)$ is slowly-increasing in the sense above.
140
+
\end{itemize}
141
+
\end{definition}
68
142
143
+
Automorphic forms form a typically infinite-dimensional vector space.
144
+
145
+
\begin{definition} An automorphic form is \emph{cuspidal} (or ``a cusp form'') if it furthermore satisfies $\int_{U(N)\U(\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.
146
+
\end{definition}
147
+
148
+
The cuspidal automorphic forms form a complex subspace of the space of automorphic forms.
149
+
150
+
\begin{definition} The group $G(\A_N)$ acts on itself on the right, and this induces a left action of its
151
+
subgroup $G(\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(\A_N^f)\times U_\infty,\mathfrak{g})$-modules.
152
+
\end{definition}
153
+
154
+
\begin{theorem} The cusp forms decompose as a (typically infinite) direct sum of irreducible $(G(\A_N^f)\times U_\infty,\mathfrak{g})$-modules.
155
+
\end{theorem}
156
+
\begin{definition} A cuspidal automorphic representation is an irreducible $(G(\A_N^f)\times U_\infty,\mathfrak{g})$-module isomorphic to an irreducible summand of the space of cusp forms.
157
+
\end{definition}
158
+
159
+
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.
160
+
161
+
\begin{definition} An automorphic representation is an irreducible $(G(\A_N^f)\times U_\infty,\mathfrak{g})$-module isomorphic to an irreducible subquotient of the space of automorphic forms.
162
+
\end{definition}
163
+
164
+
Admissibility is a finiteness condition on an irreducible representation of $(G(\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.
165
+
166
+
167
+
\begin{theorem} An irreducible admissible $(G(\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$.
168
+
\end{theorem}
169
+
\begin{proof} See Flath's article in~\cite{corvallis1}.
170
+
\end{proof}
171
+
172
+
As mentioned above, we only need all of this for abelian algebraic groups and for inner forms of $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).
173
+
174
+
\definition{}
69
175
70
176
**TODO** write this properly.
71
177
@@ -91,11 +197,4 @@ \section{Automorphic forms and representations}
91
197
92
198
Moret-Bailly
93
199
94
-
Artin symbol of local class field theory
95
-
96
-
Existence of solvable extension avoiding a global extension and with prescribed local behaviour
0 commit comments