GL(n)

Stream: maths

[Heather Macbeth]

I have PR'd (#3639) that in a normed algebra, the map $x \mapsto x^{-1}$ is smooth. With this, together with #3210, #3282, #3442, #3529, I think it should be possible to prove that $GL(n)$ is a Lie group!

I have no immediate plans to do this (instead I am working on the smooth inverse function theorem, for which these are also needed), so someone else (with @Nicolò Cavalleri the obvious candidate) should feel free to take this on.

[Nicolò Cavalleri]

Haha thank you very much I will indeed take this on :wink:

[Heather Macbeth]

By the way, it should be no extra work to show that for any complete normed algebra, the group of units is a Lie group. The other Lie groups one gets this way do not seem especially inspiring ($\mathbb{R}^+\times SU(2)$ from the quaternions, $\mathbb{R}^*\times \operatorname{Aff}(1)$ from the $2\times 2$ upper-triangular matrices, etc), but they do extend the class of examples somewhat.

[Kevin Buzzard]

How about the classical groups ie symplectic, orthogonal and unitary? How about the exceptional Lie groups eg E8 or G2?

[Heather Macbeth]

For most of these, one requires the smooth implicit function theorem (which I am :working_on_it: ). That's the technical tool to prove that the level sets of a well-behaved function are a (sub)manifold.

[Heather Macbeth]

For example, for the orthogonal group, you need that a level set of the function $A \mapsto A^t A$ is a submanifold; for the special linear group, you need that a level set of the determinant function is a submanifold.

[Heather Macbeth]

Whereas, for $GL(n)$ and the other examples I listed above, they can be written as open subsets of some $\mathbb{R}^N$, so their manifold structure comes for free!

[Nicolò Cavalleri]

I made a PR with the little work I did this summer on this!

[Kevin Buzzard]

My understanding is that SL(n) and the classical groups (orthogonal, symplectic, unitary) will be harder -- but if Heather can do U(1) then I am optimistic that everything should be possible, at least soon...

[Bryan Gin-ge Chen]

(Link to PR: #6981)

[Roman Bars]

Would it be hard to do reductive group schemes?

[Johan Commelin]

@Roman Bars What is your definition of reductive group scheme?

[Johan Commelin]

Linear affine groups over a field are probably within reach (the definition) but it will be hard to prove much about them. Otherwise, we first need a lot more general API for schemes. Currently we don't even have products of schemes, so you get stuck trying to talk about the multiplication map on a group scheme.

[Roman Bars]

I meant the definition as in http://math.stanford.edu/~conrad/papers/luminysga3smf.pdf

Let S be a scheme. An S-torus is an S-group T → S of multiplicative type with smooth connected fibers. A reductive S-group is a smooth S-affine group scheme G → S such that the geometric fibers Gs are connected reductive groups. A semisimple S-group is a reductive S-group whose geometric fibers are semisimple.

[Johan Commelin]

Roman Bars said:

I meant the definition as in http://math.stanford.edu/~conrad/papers/luminysga3smf.pdf

Let S be a scheme.

We can do that.

An S-torus is an S-group T → S

Like I said, we don't have (fibre) products of schemes, so it's not clear how to express S-group. Maybe via functor of points?

of multiplicative type

needs a def

with smooth connected fibers.

connected is fine, but smooth will require some work

A reductive S-group is a smooth S-affine group scheme G → S such that the geometric fibers Gs are

most of these ingredients will be ok, once we have resolved the issues flagged above

connected reductive groups.

So you need "reductive group over an algebraically closed field".

A semisimple S-group is a reductive S-group whose geometric fibers are semisimple.

So you need "semisimple over an alg. closed field".

[Kevin Buzzard]

If you're doing this properly you will also need to check things like a group scheme over a field becomes semisimple over an alg closure iff it becomes semisimple over all alg closures iff it becomes semisimple over an arbitrary alg closed extension. In fact I've never really known what a geometric point is -- in char p should one be using separable closures instead? All this looks to me like it's accessible but will need a ton of work. We have schemes but nobody did anything with them yet so we don't even know if the definition is usable

[Adam Topaz]

I think the first next thing to build with schemes is the fibered products.