General linear group (and special linear group)

Stream: mathlib4

[Antoine Chambert-Loir]

In mathlib, the general linear group exists

• for matrices, as the unit elements of the matrices (although the docstring says otherwise)
• and accordingly for modules, docs#LinearMap.GeneralLinearGroup, the invertible linear maps from a module to itself
  but it could have been defined for modules, as the linear equivalences from a module to itself. Is there a reason why not?

On the other hand, the special linear group only exists for matrices, as docs#Matrix.SpecialLlinearGroup, a subtype of docs#Matrix (hence the group structure is not obvious).
The question stems out my trying to define the special linear group for a module, where the easiest definition consists in taking a subtype of the type of linear equivalences, rather than of linear maps.

[Kenny Lau]

but how do you say "determinant = 1" for modules?

[Antoine Chambert-Loir]

docs#LinearMap.det

[Kenny Lau]

it might not be a group unless the module is finite and free

[Antoine Chambert-Loir]

hence my desire to define it as a subtype of the type of linear equivalences!

[Aaron Liu]

wait so what happens if the module isn't finite and free

[Bryan Wang]

If there is no finite basis on the module then LinearMap.det defaults to 1

[Antoine Chambert-Loir]

… which is OK to define a group and remove the necessity to check one additional hypothesis.

[Aaron Liu]

so what should the special linear group be

[Antoine Chambert-Loir]

I don't mind in that case. The point is to have a definition which doesn't rely on too much hypotheses and is simple enough to start the story.

[Aaron Liu]

isn't the special linear group also characterized as the quotient of the general linear group by the image of the units by the algebra map was there something like that

[Aaron Liu]

does that give you something meaningful over not a field

[Antoine Chambert-Loir]

No, you would get the projective linear group, which is close to the special linear group, but definitely different.

[Aaron Liu]

oh I guess I got my matrices mixed up

[Aaron Liu]

I give up this matrix stuff is too complicated for now

[Matthew Ballard]

You might have been thinking about their associated Lie algebras.

[Aaron Liu]

maybe I was maybe I wasn't

[Aaron Liu]

I still barely understand lie algebras

[Floris van Doorn]

I think it's bad that docs#LinearMap.GeneralLinearGroup is not defined using docs#LinearEquiv. It probably should be, analogously to docs#Equiv.Perm.

[Antoine Chambert-Loir]

As pointed out by @Moritz Doll , it would be useful to clarify the general design that we wish to have for the classical groups. He mentioned that the unitary group docs#Matrix.unitaryGroup is a submonoid of the monoid of matrices.

[Kenny Lau]

is the 0-th roots of unity of M, M or Units M? (ignore the actual definition in mathlib)

[Antoine Chambert-Loir]

docs#rootsOfUnity is a subgroup of docs#Units.

[Kenny Lau]

ignore the actual definition in mathlib

[Antoine Chambert-Loir]

I am pretty sure that this borderline case doesn't exist in standard math, so mathlib can choose what is best. I believe it would be better to have an instance that rootsOfUnity M is a group, and then Units Mis forced.

[Kenny Lau]

well in standard maths you also don't think about whether SLn is a subset of GLn or Mn^x or Mn

[Kenny Lau]

i think there's a tradeoff in both cases, since subtypes of "subtypes" are hard to work with (I know Units M isn't a subtype of M), but the instances are easier

[Antoine Chambert-Loir]

This is not the same question: you asked whether the 0-roots of unity of a monoid M were Mor Units M; in the former case, it won't be a group unless Mis.

[Antoine Chambert-Loir]

So maybe you wished to ask whether rootsOfUnity 0 M should be a subtype of M or of Units M?

[Kenny Lau]

it's a similar question where we have to choose between subtype of M or subtype of Units M

[Kenny Lau]

yes, "should be" is what i meant

[Antoine Chambert-Loir]

Definitely, but this is not what you asked (you missed subtype).

[Stepan Nesterov]

A complete Bourbaki generality definition of det would be:
If P is a finitely generated projective module over R, then the function rk(p) = dim(P \otimes Frac(R/p)) is locally constant on Spec R, and bounded by the number of generators. Let R = \Prod_{i} R_i, where Spec(R_i) = {p : rk(p) = i}. Define det(P) = \Prod_{i} \Bigwedge^i P \otimes R_i.
Then det(P) is an invertible R-module. If f : P \to P is an invertible linear map, then det(f) : det(P) \to det(P) to be a unique \lambda such that det(f) is multiplication by \lambda.
Then you can define SL(P) correctly for any finitely generated projective P.

[Kenny Lau]

is the product finite?

[Stepan Nesterov]

Kenny Lau said:

is the product finite?

Yes because the rank never exceeds the number of generators of P.

[Kenny Lau]

I look forward to seeing this in mathlib :slight_smile:

[Kenny Lau]

Stepan Nesterov said:

If f : P \to P is an invertible linear map, then det(f) : det(P) \to det(P) to be a unique \lambda such that det(f) is multiplication by \lambda.

does this step require f to be invertible?

[Antoine Chambert-Loir]

(That's perfectly correct, but doesn't address the question, and it would be excellent to have this generalization of docs#LinearMap.det, but this is off topic.)

[Kenny Lau]

maybe we can start with this part: can we prove that every map M -> M where M is an invertible module is a scalar multiplication? (edit: yes i think this is fine, because you can tensor with M' to get a map R -> R, which must be a scalar multiplication)

[Stepan Nesterov]

Kenny Lau said:

Stepan Nesterov said:

If f : P \to P is an invertible linear map, then det(f) : det(P) \to det(P) to be a unique \lambda such that det(f) is multiplication by \lambda.

does this step require f to be invertible?

No it does not. I was just trying to define SL, and then you would need a lemma which is saying that det carries invertible modules to invertible elements. Which is an obvious corollary of det(fg)=det(f)det(g), so I guess it didn't need stating.

[Johan Commelin]

Let's have a poll about how GeneralLinearGroup should be defined. Because it's hard to glean consensus from the above discussion.

[Johan Commelin]

/poll how should GeneralLinearGroup be defined

• As Units of the endomorphism ring
• Using LinearEquiv

[Edward van de Meent]

(i just want to note that docs#MulAut (the group of automorphisms of a group/monoid) uses MulEquiv, so using an "EquivLike" structure in this kind of place is not exactly untrodden path)

[Filippo A. E. Nuccio]

Ok, I confess that seeing such strong consensus scares me a bit in voting differently, but I had, so let me write down my main arguments:

1. It seems to me that GL is a gadget for which one can equally well try to prove membership or consider terms on their own (unlike many other structures for which one of the two occurs much more often than the other) and the Unit API allows this better than the LinearEquiv one;
2. Certain operations that are quite natural, like taking the direct limit over the dimension when defining K-theory, would require a strange operation on the modules if we carry them along in order to use LinearEquiv;
3. When considering it as a group scheme, or even just a group-valued functor on rings, I would imagine the library to be already sufficiently complicated to make users wishing they can forget that a category of rings comes with its associated category of modules;
4. Extending scalars gives immediately a map on matrices, and the API for units allows to basechange GL very easily. But I fear some kind of diamond if it gets a group structure both as LinearEquiv wrt the smallest ring and as LinearEquiv wrt the largest one, but that stabilize a lattice.

On the other hand, what I wrote are arguments that (might) apply to GL_n, not to GL(V), and I agree that this would certainly need to be in Mathlib.

[Antoine Chambert-Loir]

Despite my inclination towards LinearEquiv, I would like to note that it is important to use GeneralLinearGroup as a group, ie, using * for multiplication, and not .trans, 1 for id, etc. Using LinearEquiv rapidly leads to two concurrent notations.

[Johan Commelin]

@Filippo A. E. Nuccio Thanks for your careful arguments!

I think your final sentence is important, and points out that maybe my poll should be more fine-grained: what to do for GL_n, and what to do for GL(V).

And another takeaway is that whatever definition we end up with (in both instances of GL), we should make sure that the API makes it as easy as possible to also take the other POV.

[Johan Commelin]

/poll How should the general linear group GL(V) be defined, for modules V

• As Units of LinearMap V V
• As LinearEquiv V V

[Johan Commelin]

/poll How should the matrix group GL_n be defined (for a fintype n)

• As Units of Matrix n n R (current implementation)
• As a subtype of Matrix n n R, consisting of those matrices that are IsUnit

[Antoine Chambert-Loir]

I am conflicted: I would simultaneously like to vote LinearEquiv for the first case, Units for the second, and that my two votes coincide.

[Kevin Buzzard]

Maybe we need a new InvertibleMatrix type with a coercion to Matrix :-)

[Filippo A. E. Nuccio]

Antoine Chambert-Loir said:

I am conflicted: I would simultaneously like to vote LinearEquiv for the first case, Units for the second, and that my two votes coincide.

What do you mean by "coincide"? I agree that it will be important to have a smooth translation from one to the second whenV is free, but beyond that the two votes are a bit independent, no?

[Kevin Buzzard]

I would imagine that "coincide" means "if I've proved a theorem about GL(V) then I would like it apply to GL_n(R) in a completely painless fashion", a property which the solution we're tending to in the current poll would not have.

[Filippo A. E. Nuccio]

Well, I agree, but I think it's clear that it won't probably be "completely painless": we might hope that it is "extremely smooth", or the like. No?

[Kevin Buzzard]

If they're both defined as Units then it probably will be completely painless. Hmm, yes, even if they're both Units, we then run into the issue that we have to translate between Matrix and LinearMap. So probably you're right, we just need to make the isomorphism and having them both as Units doesn't make it rfl.

[Filippo A. E. Nuccio]

Yes, I think that one way or another the path would be through AddAut.toPerm (to interpret automorphisms as permutations) and then Equiv.Perm.equivUnitsEnd to interpret the latter as a unit.

[Filippo A. E. Nuccio]

But it would be reasonably smooth, as it is now, where some of these morpshism are coercions and invisible to users.

[Antoine Chambert-Loir]

In my mind, $n \times m$ matrices are (meaning exactly, without any coercion or interpretation or whatever) the linear maps from $R^m$ to $R^n$.

[Kevin Buzzard]

Well that's going to be quite some refactor!

[Riccardo Brasca]

Note that docs#Matrix is defined for any type α (why the doc says R if it is α in the code?!), without any operation.

You can say that this generality is a joke, and I agree, but it captures the intuition "matrices of real numbers are just tables of real numbers", that in my opinion is quite good.

[Riccardo Brasca]

Anyway, I don't think we should stress too much about matrices (we should not ignore them either of course): once the basic API is there mathlib should concentrate on linear maps/equiv and use matrices only when needed in proofs.

[Filippo A. E. Nuccio]

Well, but for algebraic purposes (as in studying representations of semi simple algebras) they might be your main focus. So I'm not sure to fully agree.

[Riccardo Brasca]

OK, maybe I was a little too drastic, but my point is that if the transition works well for the base theory we can develop linear maps without spending too much time in keeping the two APIs perfectly aligned.

[Filippo A. E. Nuccio]

I' ve just realised (and I apologise if that was already clear to everyone) that we've got both docs#Matrix.GeneralLinearGroup (with notation GL) and docs#LinearMap.GeneralLinearGroup (but with no dedicated notation), both defined as units of the relative ring: in the latter case it is (M →ₗ[R] M)ˣ and docs#LinearMap.GeneralLinearGroup.generalLinearEquiv shows that these units are also (multiplicatively) isomorphic to M ≃ₗ[R] M. I'm not sure I would change things, beyond perhaps

1. Providing some more docs beyond the "See also docs#Matrix.GeneralLinearGroup " at the begginning of Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
2. Providing the isomorphism between the Matrix and the LinearMap in case of a free module
3. Perhaps most importantly, allowing the GL notation for both, as scoped notation, so that one can choose which to use and where.

[Riccardo Brasca]

I think the idea is to get rid of LinearMap.GeneralLinearGroup

[Filippo A. E. Nuccio]

Yes yes, I understand, but I'm saying that with appropriate doc I would not see the need for this removal after all.

[Riccardo Brasca]

The reason is that we have two notions that are mathematically exactly the same thing (I am talking about linear equiv and LinearMap.GeneralLinearGroup, not matrices)

[Filippo A. E. Nuccio]

Ah, you mean that you would like to define LinearMap.GeneralLinearGroup as linear equiv on the nose, rather than as units of the endomorphism ring of the module, so that the multiplicative equiv is not needed any more?

[Riccardo Brasca]

Yes, something like that. What is the advantage of LinearMap.GeneralLinearGroup? The * notation?

[Filippo A. E. Nuccio]

Ah, then I 100% agree.

[Filippo A. E. Nuccio]

(Yes, the * notation is handy, but it can probably simply be forced in a dedicated namespace, no?)

[Filippo A. E. Nuccio]

My only point was that we certainly want to keep Matrix.GeneralLinearGroup, and to define it as units of the matrix algebra.

[Riccardo Brasca]

Sure, for matrices this seems the best approach

[Riccardo Brasca]

Well, there is the question if we want them to be a submonoid of matrices, but I would say no. On the other hand SL should be a subgroup of GL in my opinion.

[Filippo A. E. Nuccio]

Them?

[Riccardo Brasca]

GL would be a new type, not a submonoid of Mat. But the same happens for Rˣ and R so it should be good.

[Riccardo Brasca]

This is probably good also to compute the inverse, since M⁻¹ will be packaged inside M : GL