7. Automorphic forms and the Langlands Conjectures
7.1. Definition of an automorphic form for GLn over Q
The global Langlands reciprocity conjectures relate automorphic forms to Galois
representations. The statements for a general connected reductive group involve
the construction of the Langlands dual group, and we do not have quite enough
Lie algebra theory to push this definition through in general. However if we
restrict the special case of the group \GL_n/\Q, the dual group is just
\GL_n(\bbC) and several other technical obstructions are also removed. In
this section we will explain the definition of an automorphic form for the
group \GL_n/\Q, following the exposition by Borel and Jacquet in Corvallis
(volume, 1979).
7.2. The Finite Adeles Of The Rationals
Mathlib already has the definition of the finite adeles \A_{\Q}^f of the
rationals as a commutative \Q-algebra, and the proof that it's a
topological ring.
7.3. The Group GLn Of The Adeles
The adeles \A_{\Q} of \Q are the product \A_{\Q}^f \times \R, with the
product topology. They are a topological ring. Hence
\GL_n(\A_{\Q}) = \GL_n(\A_{\Q}^f) \times \GL_n(\R) is a topological group,
where we are being a bit liberal with our use of the equality symbol.
7.4. Smooth Functions
- No associated Lean code or declarations.
A function f : \GL_n(\A_{\Q}^f) \times \GL_n(\R) \to \bbC is smooth if it has
the following three properties:
-
fis continuous. -
For all
x \in \GL_n(\A_{\Q}^f), the functiony \mapsto f(x,y)is smooth. -
For all
y \in \GL_n(\R), the functionx \mapsto f(x,y)is locally constant.
Current state of this definition: I've half-formalised it; I don't know how to say the the function is smooth on the infinite part, because I have never used the manifold library before and I have no idea what my model with corners is supposed to be.
7.5. Slowly-Increasing Functions
Automorphic representations satisfy a growth condition which we may as well factor out into a separate definition.
We define the following temporary "size" function s : \GL_n(\R) \to \R
by s(M) = \operatorname{trace}(MM^T + M^{-1}M^{-T}), where M^{-T}
denotes inverse-transpose. Note that s(M) is always positive, and is large
if M has a very large or very small, in absolute value, eigenvalue.
-
AutomorphicForm.GLn.IsSlowlyIncreasing[complete]
We say that a function f : \GL_n(\R) \to \bbC is slowly-increasing if there
is some real constant C and positive integer n such that
|f(M)| \leq C s(M)^n for all M \in \GL_n(\R).
Lean code for Definition7.5.1●1 definition
Associated Lean declarations
-
AutomorphicForm.GLn.IsSlowlyIncreasing[complete]
-
AutomorphicForm.GLn.IsSlowlyIncreasing[complete]
-
structuredefined in FLT/GlobalLanglandsConjectures/GLnDefs.leancomplete
structure AutomorphicForm.GLn.IsSlowlyIncreasing {n : ℕ} (f : GL (Fin n) ℝ → ℂ) : Prop
structure AutomorphicForm.GLn.IsSlowlyIncreasing {n : ℕ} (f : GL (Fin n) ℝ → ℂ) : Prop
A function `f : GL_n(ℝ) → ℂ` is slowly increasing if there exist `C, N` such that `‖f M‖ ≤ C · s(M)^N` for all `M`, where `s` is an auxiliary "size" function.
Fields
bounded_by : ∃ C N, ∀ (M : GL (Fin n) ℝ), ‖f M‖ ≤ C * AutomorphicForm.GLn.s ↑M ^ N
Note: the book says n is positive, but \{M|s(M)\leq 1\} is compact so I
don't think it makes any difference.
7.6. Weights At Infinity
-
AutomorphicForm.GLn.Weight[complete]
The weight of an automorphic form for \GL_n/\Q can be thought of as a
finite-dimensional continuous complex representation \rho of a maximal
compact subgroup of \GL_n(\R), and it's convenient to choose one (they're
all conjugate) so we choose O_n(\R).
Lean code for Definition7.6.1●1 definition
Associated Lean declarations
-
AutomorphicForm.GLn.Weight[complete]
-
AutomorphicForm.GLn.Weight[complete]
-
structuredefined in FLT/GlobalLanglandsConjectures/GLnDefs.leancomplete
structure AutomorphicForm.GLn.Weight (n : ℕ) : Type
structure AutomorphicForm.GLn.Weight (n : ℕ) : Type
A weight for `GLₙ`: a preweight whose associated `O(n)`-representation is simple.
Fields
w : AutomorphicForm.GLn.preweight n
The underlying preweight, i.e. continuous representation of `O(n)`.
isSimple : CategoryTheory.Simple (AutomorphicForm.GLn.preweight.fdRep n self.w)
The Lean definition is incomplete right now -- I don't demand irreducibility (I wasn't sure whether I was doing this the right way; if I used category theory then I might have struggled to say that the representation was continuous).
7.7. The Action Of The Universal Enveloping Algebra
- No associated Lean code or declarations.
There is a natural action of the real Lie algebra of \GL_n(\R) on the
complex vector space of smooth complex-valued functions on \GL_n(\R).
This extends to a natural complex Lie algebra action of the complexification of
the real Lie algebra on the smooth complex-valued functions on \GL_n(\R).
This depends on Definition 7.7.1.
By functoriality, we get an action of the universal enveloping algebra of this complexified Lie algebra on the smooth complex-valued functions. This depends on Definition 7.7.2.
Thus the centre Z_n of this universal enveloping algebra also acts on the
smooth complex-valued functions. This depends on
Definition 7.7.3.
The centre we just defined is a commutative ring which contains a copy of
\bbC. Note that Harish-Chandra, or possibly this was known earlier, showed
that it is a polynomial ring in n variables over the complexes. We shall not
need this.
7.8. Automorphic Forms
From here on there is no more Lean right now, only LaTeX.
A smooth function f : \GL_n(\A_{\Q}^f) \times \GL_n(\R) \to \bbC is an
O_n(\R)-automorphic form on \GL_n(\A_{\Q}) if it satisfies the following
five conditions. This depends on Definition 7.4.1,
Definition 7.5.1,
Definition 7.6.1, and Definition 7.7.4.
-
Periodicity: for all
g \in \GL_n(\Q), we havef(gx,gy) = f(x,y). -
It has a finite level: there exists a compact open subgroup
U \subseteq \GL_n(\A_{\Q}^f)such thatf(xu,y) = f(x,y)for allu \in U,x \in \GL_n(\A_{\Q}^f), andy \in \GL_n(\R). -
It has weight
\rho: there exists a continuous finite-dimensional irreducible complex representation\rhoofO_n(\R)such that for every(x,y) \in \GL_n(\A_{\Q}), the complex vector space spanned by the functionsk \mapsto f(x,yk)is finite-dimensional and isomorphic, as anO_n(\R)-representation, to a direct sum\rho^{\oplus m}of copies of\rhofor somem. -
It has an infinite level: there is an ideal
I \subseteq Z_nof the centreZ_ndescribed in the previous section, with finite complex codimension, andIannihilates the functiony \mapsto f(x,y)for allx \in \GL_n(\A_{\Q}^f). This is a very fancy way of saying that the function satisfies some natural differential equations. In the case of modular forms, these are the Cauchy-Riemann equations, which is why modular forms are holomorphic. -
It satisfies the growth condition: for every
x \in \GL_n(\A_{\Q}^f), the functiony \mapsto f(x,y)on\GL_n(\R)is slowly-increasing.
Lean code for Definition7.8.1●1 definition
Associated Lean declarations
-
structuredefined in FLT/GlobalLanglandsConjectures/GLnDefs.leancomplete
structure AutomorphicForm.GLn.AutomorphicFormForGLnOverQ (n : ℕ) (ρ : AutomorphicForm.GLn.Weight n) : Type
structure AutomorphicForm.GLn.AutomorphicFormForGLnOverQ (n : ℕ) (ρ : AutomorphicForm.GLn.Weight n) : Type
Automorphic forms for GL_n/Q with weight ρ.
Fields
toFun : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ
The underlying function `GL_n(𝔸_f) × GL_n(ℝ) → ℂ`.
is_smooth : AutomorphicForm.GLn.IsSmooth self.toFun
is_periodic : ∀ (g : GL (Fin n) ℚ) (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)) (y : GL (Fin n) ℝ), self.toFun (((algebraMap ℚ (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)).GL (Fin n)) g * x, ((algebraMap ℚ ℝ).GL (Fin n)) g * y) = self.toFun (x, y)
is_slowly_increasing : ∀ (x : GL (Fin n) (IsDedekindDomain.FiniteAdeleRing ℤ ℚ)), AutomorphicForm.GLn.IsSlowlyIncreasing fun y ↦ self.toFun (x, y)
has_finite_level : ∃ U, AutomorphicForm.GLn.IsConstantOn U self.toFun
Automorphic forms of a fixed weight \rho form a complex vector space, and if
we also fix the finite level U and the infinite level I then we get a
subspace which is finite-dimensional; this is a theorem of Harish-Chandra.
There is also the concept of a cusp form, meaning an automorphic form for which
furthermore some adelic integrals vanish.
7.9. Hecke Operators
- No associated Lean code or declarations.
The group \GL_n(\A_{\Q}^f) acts on the space of automorphic forms for
\GL_n(\A_{\Q}) by the formula (g \cdot f)(x,y) = f(xg,y).
This is obvious. Note that the conjugate of a compact open subgroup is still compact and open.
A formal development of the theory of Hecke operators looks like the following.
Let U be a fixed compact open subgroup of \GL_n(\A_{\Q}^f), and let us
also fix a weight \rho. Let M_\rho(n) denote the complex vector space of
automorphic forms for \GL_n/\Q of weight \rho. The level U forms
M_\rho(n,U) are just the U-invariants of this space. If
g \in \GL_n(\A_{\Q}^f), then the double coset space UgU can be written as
a finite disjoint union of single cosets g_iU: the double coset space is
certainly a disjoint union of left cosets, but the double coset space is
compact and the left cosets are open.
Define the Hecke operator T_g : M_\rho(n,U) \to M_\rho(n,U) by
T_g(f) = \sum g_i \cdot f.
- No associated Lean code or declarations.
This function is well-defined, i.e. it sends a U-invariant form to a
U-invariant form which is independent of the choice of g_i.
Easy group theory.