Kevin Buzzard (Feb 18 2020 at 22:02):
About ten to 15 years ago I tried to get a straight answer to the question: "what is the definition of an automorphic representation of a connected reductive group over a number field?" and I ended up somehow convincing myself that to understand the definition you needed to understand the theory of direct integrals of representations of groups like on certain Hilbert spaces. I did not know this theory and ever since then I've been telling people that I have written papers about automorphic representations and I don't even know what they are.
I visited Durham a few weeks ago and was explaining all this to my my eldest mathematical grandson, Jack Shotton, and he pointed out that an automophic representation was just a subquotient and you didn't have to worry about all the direct integral stuff.
I have finally got around to googling, and he's right. Furthermore I've found a really good source for the definition in full generality, and it's this. I think it does a really good job of explaining the definition right down to the mathematical nuts and bolts. I think it would be a really interesting formalisation project.
A couple of things which the computer scientists might find amusing: check out the definition of an automorphic representation (definition 3.10) on p19. It's a representation of something called . Now check out section 5.5 -- "an alternate definition"! It's now a module for a completely different thing. The two types have a canonical
equiv which we all believe, so people refer to both types as automorphic representations. Some proof techniques are more amenable to one "representation" than the other.
The proof that the arrows of the
equiv are inverse to each other is "a result due to Harish-Chandra", for which we are given no reference, or even an idea of how deep the result is. Let me note that this is not a criticism of the notes! I have no doubt that this is a standard theorem and any expert could tell you a proof and a reference. It's just funny that it's not there and you can't do that in computer science.
Kevin Buzzard (Feb 18 2020 at 22:14):
This is just the sort of reason that we had to work in the perfectoid project to make a definition. There can be two equiv types
Y, and maybe the map
f : X -> Y is easy to define, but defining the (noncomputable) inverse is equivalent to proving the deep theorem that
f is a bijection. Now say you want to define a function on
Y -> Yand you want to pull back a function on
X -> X, but we can't build the map
(Y -> Y) -> (X -> X) without proving the theorem needed to define the
equiv. In particular, we can't say "a perfectoid space is a Y such that all Y -> Y have property P defined on X's" without proving a theorem.
Kevin Buzzard (Feb 18 2020 at 22:17):
Sometimes we worked to fill in the proofs, and sometimes we bent the truth, defining a perfectoid space to be an X such that all maps X -> X have property P, and if someone asks us how come our definition is the same as Scholze's, we can point them to "a result due to Harish-Chandra" or whatever.
Kevin Buzzard (Feb 18 2020 at 22:22):
Interestingly, I would occasionally point at Torsten Wedhorn's adic spaces notes (available on his website) when justifying that our definition was the same as Scholze's, and then they just randomly disappeared off the internet when he moved institution. Me and other people urged him to get them back out there and he very kindly put them up on ArXiv. But what we have now doesn't rely on any results whose proof is only in Wedhorn -- we can always point back to some trusted place in the established published literature.
Kevin Buzzard (Feb 18 2020 at 23:06):
An example of a map which it's hard to prove is bijective is the map from the type of isomorphism classes of locally compact Hausdorff topological abelian groups to itself defined by "take the pontrjagin dual, and then take it again". It's a hard theorem that the canonical map from G to its double dual is an isomorphism.
Kevin Buzzard (Feb 18 2020 at 23:07):
Assuming the theorem feels a bit like assuming the law of the excluded middle, although it bothers me a lot more!
Kevin Buzzard (Feb 18 2020 at 23:08):
The inverse map is like a map from not not G to G
Kevin Buzzard (Feb 18 2020 at 23:15):
I think the proof in Ramakrishnan-Valenza is at least a chapter long
Kevin Buzzard (Feb 18 2020 at 23:16):
And it uses a tonne of other stuff
Reid Barton (Feb 19 2020 at 01:29):
It probably even uses lem
Kevin Buzzard (Feb 19 2020 at 01:43):
Almost certainly :-)
Kevin Buzzard (Feb 19 2020 at 01:44):
Both lem and harmonic analysis
Last updated: May 11 2021 at 15:12 UTC