GL(n) as a manifold

Stream: Is there code for X?

[Dominic Steinitz]

These instances did not seem to exist

-- #synth  ChartedSpace (EuclideanSpace ℝ (Fin (n * n))) (GeneralLinearGroup (Fin n) ℝ)
-- #synth IsManifold (𝓡 (n * n)) ⊤ (GeneralLinearGroup (Fin n) ℝ)

There a theorem that says an open subset of a space is already a charted space and manifold:

#check TopologicalSpace.Opens.instChartedSpace

But now I have to show that {A | Matrix.det A ≠ 0} is open in $\mathbb{R}^{n^2}$. I'd rather not re-invent any wheels.

[Sébastien Gouëzel]

Have you seen docs#Units.instLieGroupModelWithCornersSelf (and the neighboring instances)?

[Antoine Chambert-Loir]

On the other hand, Mathlib doesn't seem to have submanifolds yet, and Cartan's theorem would be a stronger result, wouldn't it?

[Kevin Buzzard]

Right, we need things like $SL_n(\R)$ as a Lie group, and also $E_6(\R)$ etc when these have been defined (eg as Hopf algebras or subgroups of matrix groups)

[Dominic Steinitz]

Antoine Chambert-Loir said:

On the other hand, Mathlib doesn't seem to have submanifolds yet, and Cartan's theorem would be a stronger result, wouldn't it?

I am sorry but your reply is a bit too cryptic for me. Are you saying we need submanifolds for $GL_n(\mathbb{R})$ to be a manifold? Which Cartan and which theorem?

[Dominic Steinitz]

Sébastien Gouëzel said:

Have you seen docs#Units.instLieGroupModelWithCornersSelf (and the neighboring instances)?

I have not but will look now.

[Dominic Steinitz]

Sébastien Gouëzel said:

Have you seen docs#Units.instLieGroupModelWithCornersSelf (and the neighboring instances)?

The example given is

import Mathlib

open Matrix Set
open scoped Manifold
open SmoothManifoldWithCorners

example {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] :
  LieGroup 𝓘(ℝ, V →L[ℝ] V) ⊤ (V →L[ℝ] V)ˣ := inferInstance

variable {n : ℕ}

#synth Group (Matrix.GeneralLinearGroup (Fin n) ℝ)
#synth Group (LinearMap.GeneralLinearGroup ℝ (Fin n → ℝ))

#synth AddGroup (Matrix.GeneralLinearGroup (Fin n) ℝ)
#synth AddGroup (LinearMap.GeneralLinearGroup ℝ (Fin n -> ℝ))

but the GeneralLinearGroup is not even an AddGroup.

I am not sure how to proceed. Should I add instances for GeneralLinearGroup? Is this approach better than just saying that $GL_n(\mathbb{R})$ is open in $\mathbb{R}^{n^2}$.

I want $GL_n(\mathbb{R})$ to be a Lie group to define the fundamental vector field. I'd like a concrete Lie group and its corresponding algebra (which I found on this branch).

[Sébastien Gouëzel]

I'm not sure I understand your question. Sure, GeneralLinearGroup is not an AddGroup: what would be the sum of I and -I, say?

[Dominic Steinitz]

Sébastien Gouëzel said:

I'm not sure I understand your question. Sure, GeneralLinearGroup is not an AddGroup: what would be the sum of I and -I, say?

Yes but the example given in the reference you pointed me to (thanks for that) required this. Ah I just realised that you meant something else and not that example. Let me think a bit more.

[Michael Rothgang]

GeneralLinearGroup is a Group - the group operation is multiplication, not addition.

[Michael Rothgang]

About submanifolds: I'm slowly working on them (travelling now and dealing with technology... fun); hopefully I can open a first PR next week.

[Michael Rothgang]

That said, you shouldn't need this to talk about GL(n).

[Dominic Steinitz]

I have GL(n) is a Lie group so it must be a manifold.

import Mathlib

open Matrix
open scoped Manifold

variable {n : ℕ}

noncomputable
instance : NormedRing (Matrix (Fin n) (Fin n) ℝ) := frobeniusNormedRing

noncomputable
instance : NormedAlgebra ℝ (Matrix (Fin n) (Fin n)  ℝ) := frobeniusNormedAlgebra

example : LieGroup 𝓘(ℝ, (Matrix (Fin n) (Fin n)  ℝ)) n (Matrix (Fin n) (Fin n)  ℝ)ˣ :=
  inferInstance

example : (Matrix (Fin n) (Fin n)  ℝ)ˣ = GeneralLinearGroup (Fin n) ℝ := rfl

[Dominic Steinitz]

But I am still mystified. I was expecting the ModelWithCorners to be 𝓡 (n * n) but there is not even a ChartedSpace instance (the second synth fails).

#synth  ChartedSpace (Matrix (Fin n) (Fin n) ℝ) (GL (Fin n) ℝ)

#synth  ChartedSpace (EuclideanSpace ℝ (Fin (n * n))) (GL (Fin n) ℝ)

[Antoine Chambert-Loir]

Dominic Steinitz said:

Antoine Chambert-Loir said:

On the other hand, Mathlib doesn't seem to have submanifolds yet, and Cartan's theorem would be a stronger result, wouldn't it?

I am sorry but your reply is a bit too cryptic for me. Are you saying we need submanifolds for $GL_n(\mathbb{R})$ to be a manifold? Which Cartan and which theorem?

Saying that a subspace is a submanifold means that it has local coordinates given by a subset of local coordinates of the ambiant space. A criterion for that is to be definable by $c$ equations of class $\mathscr C^1$ whose differentials are linearly independent at each point of the subspace. (If one works locally, this is even a necessary condition.)

The theorem of Cartan says that every closed subgroup of a Lie group (for example $GL(n,\mathbf R)$) is a submanifold (hence a Lie group).