GL_n or GL(V)? Lie group help

Stream: FLT

[Kevin Buzzard]

The global Langlands conjectures start "let $G$ be a connected reductive group over a global field". But already the global Langlands conjectures are very deep and interesting in the special case where $G = GL_n$ and the global field is the rational numbers. The following challenge question has come up in Bonn: to formalise the definition of automorphic forms for this $G$.

I asked Patrick if we knew that $GL_n(\R)$ was a Lie group and he said it was in mathlib. I looked, and what we actually have is this:

import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

open Manifold

variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] in
#synth LieGroup 𝓘(ℝ, V →L[ℝ] V) (V →L[ℝ] V)ˣ -- Units.instLieGroupModelWithCornersSelf

This is not good enough for my application, because even though Fin n → ℝ satisfies all these typeclass criteria, the conclusion is about continuous linear maps and we want all linear maps, and furthermore the actual vector space we'll get is of the form V ⊗[ℚ] ℝ with V a finite-dimensional vector space over $\mathbb{Q}$.

So if I want to prove the global Langlands conjectures for $GL(0)/\mathbb{Q}$ I need to make one of the following things into a Lie group: The "concrete approach"

import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup

open Manifold

variable (n : ℕ)
#synth LieGroup sorry (Matrix.GeneralLinearGroup (Fin n) ℝ) -- need a local model?

or the "abstract approach"

import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

variable (V : Type) [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V]

open TensorProduct

#synth LieGroup sorry (ℝ ⊗[ℚ] V ≃ₗ[ℝ] ℝ ⊗[ℚ] V)

Right now it's difficult to go too much further because I don't know which model of GL_n I'm using. Which of these is easiest to put a Lie group structure on?

[Sébastien Gouëzel]

A Lie group needs a topology. So your first question should be: on which of these spaces can I put a natural topology (and it's related to your question in the other thread). My answer would be the same as Patrick: if you want a topology, then obviously you're working from the start with continuous linear maps, although it's not written explicitly anywhere since we're in a setting where all linear maps are continuous.

[Kevin Buzzard]

We have this:

import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

variable (n : ℕ)

#synth TopologicalGroup (Matrix.GeneralLinearGroup (Fin n) ℝ)

so one could ask for a Lie group structure on this (and as far as I know we don't have it, and I don't know how to start making it).

This doesn't work:

import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

variable (V : Type) [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
#synth TopologicalSpace (V ≃ₗ[ℝ] V)

Do we want this instance in mathlib? My "module topology" would put a topological ring structure on V →ₗ[ℝ] Vand hence a topological group structure on the units.

[Anatole Dedecker]

I think we don't want any instance which builds topology on a general (even finite dimensional) vector space from purely algebraic data.

[Anatole Dedecker]

The instance of Matrix.GeneralLinearGroup (Fin n) ℝ is fine because it is very specific (like the instance on Fin n \to ℝ), but V ≃ₗ[ℝ] V sounds too general to have an instance on it : surely if V has a weird topology (e.g non Hausdorff !) you don't want the topology on V ≃ₗ[ℝ] V to be the same.

[Anatole Dedecker]

Well okay if V has a weird topology you wouldn't want to consider V ≃ₗ[ℝ] V anyways...

[Sébastien Gouëzel]

Indeed, there is no harm in doing this on concrete matrix groups. For instance, I would be happy with

import Mathlib

variable (n : ℕ)
open Manifold

-- next line needed to turn matrix spaces into normed space, to use them as model spaces
attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace

#synth LieGroup 𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ) (Matrix.GeneralLinearGroup (Fin n) ℝ)

(For now, it doesn't work, but it shouldn't be hard to copy the implementation of Units.instLieGroupModelWithCornersSelf)

[Sébastien Gouëzel]

In fact we already have it, it's just a matter of activating the right instances:

import Mathlib

variable (n : ℕ)
open Manifold

attribute [local instance] Matrix.linftyOpNormedAddCommGroup Matrix.linftyOpNormedSpace
  Matrix.linftyOpNormedRing Matrix.linftyOpNormedAlgebra

#synth LieGroup 𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ) (Matrix.GeneralLinearGroup (Fin n) ℝ) -- works

[Jireh Loreaux]

Oh that's great! I'm so glad it's that easy.

[Eric Wieser]

It's probably time to put those instances in a scope. I'm glad they turned out to be useful!

[Anatole Dedecker]

Well, that means choosing the norm on matrices right? I’m all for it, but wasn’t this controversial?

[Yaël Dillies]

No, Eric means making them scoped, as opposed to just definitions as they are right now. He is not suggesting making them globally instances

[Kevin Buzzard]

Can I temporarily put a norm on matrices, get the Lie group structure, and then forget the norm? The definition of a differentiable map and of its derivative should be independent of the norm, right?

[Yaël Dillies]

Currently no, but yes we all agree that the derivative shouldn't depend on the norm and that we should fix this

[Sébastien Gouëzel]

For Lie groups, you need C^\infty maps or, better, analytic maps, as C^\infty will not be enough to get symmetry of the second derivative unless you're over the reals or the complexes. I don't think it really makes sense to define analytic maps if you don't have a norm (although, of course, they only depend on the norm up to norm equivalence, but in practice it's so much more comfortable to work with a norm than with an equivalence class of norms). So my advice would rather be: put all the matrix norm instances inside a scope, say MatrixLInftyNorm or whatever, and then open MatrixLInftyNorm at the beginning of the files in which you want to use the Lie group structure on matrices.

[Eric Wieser]

And while you're there, add Matrix.FrobeniusNorm and Matrix.ElementwiseNorm scopes

[Junyan Xu]

Presumably we could be talking about bornology wherever we are tempted to invoke (equivalence classes) of norms? Isn't that the plan to make derivatives independent of the norm?

[Sébastien Gouëzel]

Making derivatives independent of the norm is easy, you just need a notion of limit (with some kind of uniformity). Making analytic functions independent of a norm is another kind of business.