What's needed for automorphic forms?

Stream: mathlib4

[Kevin Buzzard]

As far as I can see, in order to make the definition of an automorphic form for a connected reductive group over a global field there are two key missing pieces: (1) definition of a reductive group (NB this is not a group, it's a group variety) and (2) real points of a smooth variety over the reals are a real manifold.

For (1) I feel like I can figure out myself what is missing, and my instinct is that we should do the Lie algebra theory first (which people like Oliver Nash are doing), but for (2) I always forget. An example of what I'm talking about: consider a symplectic or orthogonal group, as a subgroup of $GL_n(\R)$ cut out by finitely many polynomial equations. What is needed in order to make this into a real manifold? The inverse or implicit function theorem or something? Are there people working on this?

Ideally the statement would be that if X is a scheme over the reals which is smooth of relative dimension n then the set of real sections of the structure map (i.e. the real points of X) should inherit the structure of a real n-dimensional manifold. As I type this I remember that the first thing to do is to give it the structure of a topological space, for which #21283 is key.

[Andrew Yang]

For (2) I think the current hurdle is to even define submanifolds and then you want the regular value theorem (which is just a packaged version of implicit function theorem). I have talked to @Christian Merten about this, who has then talked to @Michael Rothgang who seem to have some plans.

[Christian Merten]

@Michael Rothgang is actively working on the necessary differential geometry. On the algebraic side, we should have everything.

[Andrew Yang]

On the algebraic side we still need that smooth implies regular (in the sense of the regular value theorem, i.e. differentials doesn't vanish)

[Christian Merten]

Isn't that the current definition of smooth?

[Antoine Chambert-Loir]

For (2), there is a general theorem of Élie Cartan : a closed subgroup $G$ of $\mathrm{GL}(n,\mathbf R)$ is a submanifold. The proof (in the way I teach it) goes by first exhibiting its tangent cone at identity, and showing that this is the set $\mathfrak g$ of all matrices $A\in\mathrm{Mat}(n,\mathbf R)$ such that $\exp(tA)\in G$ for all $t\in\mathbf R$. Then, the inverse function theorem for the exponential map shows that $G$ is a submanifold, with tangent space $\mathfrak g$. Also, $\mathfrak g$ is a sub-Lie-algebra of $\mathrm{Mat}(n,\mathbf R)$.

[Patrick Massot]

Formalizing Cartan’s closed subgroup theorem would be really nice.

[Antoine Chambert-Loir]

But that means formalizing submanifolds first.

[Patrick Massot]

Yes, that's long overdue.