Matrix.SpecialLinearGroup.toGL

Stream: mathlib4

[Judith Ludwig]

Matrix.SpecialLinearGroup.toGL defines "the map" from $\mathrm{SL}_n(R)$​ to $\mathrm{GL}_n(R)$​ (here $R$ is a CommRing). I expected the target of this map to be
Matrix.GeneralLinearGroup n Rand the map being the natural inclusion of groups of matrices, but instead the target is LinearMap.GeneralLinearGroup R (n → R).
Shouldn't the natural inclusion of the matrix groups be defined in mathlib (or maybe it is and I didn't find it?), and wouldn't it be good to call it Matrix.SpecialLinearGroup.toGL?

(There are maps like Matrix.SpecialLinearGroup.toGLPos, which are defined as I would have expected.)

[Eric Wieser]

That does surprise me, I'd expect the same thing as you here

[Eric Wieser]

The function you're looking for is docs#Matrix.SpecialLinearGroup.coeToGL, which is badly named

[Eric Wieser]

IMO we should drop docs#Matrix.SpecialLinearGroup.toGL entirely, and force users to translate first to the matrix GL, and then to the linear map GL, via separate maps

[Judith Ludwig]

Eric Wieser said:

The function you're looking for is docs#Matrix.SpecialLinearGroup.coeToGL, which is badly named

I guess I do claim that it would be nice to have the multiplicative map (with the map Matrix.SpecialLinearGroup.coeToGL as the underlying toFun).

(This came up when I wanted to define the restriction of an action of $\mathrm{GL}_n(R)$ on some set to the subgroup $\mathrm{SL}_n(R)$, and I was surprised I had to define the group hom first. I guess there are many other situations where the group hom would be good to have?)

[Junyan Xu]

Eric Wieser said:

IMO we should drop docs#Matrix.SpecialLinearGroup.toGL entirely, and force users to translate first to the matrix GL, and then to the linear map GL, via separate maps

I agree that this refactoring is the correct thing to do. As a temporary workaround, you may compose with the inverse of docs#Matrix.GeneralLinearGroup.toLin or docs#Matrix.GeneralLinearGroup.toLinear to get back to the world of matrices, but going back and forth between matrices and linear maps is definitely not ideal. (Note that these two decls are exact duplicates: both were added 3 years ago, the former by @Chris Birkbeck in mathlib3#8466,the latter by @Alex Kontorovich in #8611, and when doing the refactoring we should also remove one of them and use the other to do the transition between matrices and linear maps which is a part of the original docs#Matrix.SpecialLinearGroup.toGL.)

[Chris Birkbeck]

Yeah I agree, we should refactor (and remove the duplicating! sorry about that!) and leave the map into the linear version as something separate since so far in my experience its rarely used.

[Judith Ludwig]

Thanks everyone for your input on this. I've refactored as suggested in #19523.

[Junyan Xu]

Thanks! I left some comments but will wait for another reviewer (preferably original authors). It's a pretty easy PR; docs#Matrix.SpecialLinearGroup.toGL is indeed not used in Mathlib.

[Chris Birkbeck]

Thanks for doing this!