Should we change `SpecialLinearGroup` to be `Subgroup`?

Stream: mathlib4

[Wen Yang]

@Oliver Nash commented in GitHub:

I claim our definition SpecialLinearGroup should be changed and should really be defined to have type Subgroup (GeneralLinearMap R M) rather than just a Subtype. Probably we should also have a second definition which would have type Subgroup (Matrix n n R)ˣ and could be called something like SpecialLinearMatrixGroup. The main point though is that by having type Subgroup a lot of boilerplate currently in this file could be dropped.

What do you think?

[Kevin Buzzard]

docs#Matrix.SpecialLinearGroup

[Kevin Buzzard]

docs#Subgroup

[Eric Wieser]

docs#SpecialLinearGroup (doesn't exist)

[Kevin Buzzard]

It looks like we can't have subgroups of a monoid so I think Oliver is dead right.

I've just had to start working with general linear groups and we have two kinds -- matrices and endomorphisms (concrete and abstract). I think that this is necessary. And I think that for all the classical groups (special linear, symplectic, orthogonal, unitary) we're going to want two definitions -- a concrete one and an abstract one -- and they should all be subgroups of the appropriate general linear group because this is how they're used in practice.

My only reservation about this design decision is that I have seen typeclass inference go haywire recently when faced with \u|-\MCO K(the type corresponding to the integers of a number field) and so am currently a bit nervous about coerced subtypes in general, but my impression is that the community are getting on top of these issues

[Kevin Buzzard]

We have docs#Matrix.GeneralLinearGroup and docs#LinearMap.GeneralLinearGroup and I think we should follow this pattern for all the classical groups, with everything being a subgroup in each case. This is how the groups are used in practice.

[Eric Wieser]

LinearMap.GeneralLinearGroup is not a subgroup though :)

[Kevin Buzzard]

Yeah but this is the base case

[Kevin Buzzard]

The General Linear is moving from a monoid to a group and once you're in group land you never want to leave (in this part of mathematics)

[Eric Wieser]

What about things like docs#Matrix.unitaryGroup ?

[Kevin Buzzard]

I guess we'll have to talk to the unitary group people but my gut feeling is that pain will be minimised if this were a subgroup of Matrix.GeneralLinearGroup rather than a submonoid of a matrix group.

[Kevin Buzzard]

Right now there seems to be a genuine risk that the symplectic group people will come along and make a third design decision for how their subgroups of GL(n) are implemented. I suspect we're in this mess because "special linear groups" will have been an entry on the undergraduate to-do list and someone will have knocked it off just to get it out the way rather than for any other reason

[Kevin Buzzard]

I'm on mobile and can't figure out how to see if the unitary group file is a leaf file in the API docs page

[Yaël Dillies]

It is not:
image.png

[Kevin Buzzard]

Thanks. And do these files suffer with the fact that it's defined as a monoid?? It sounds like the worst of all worlds to me.

[Kevin Buzzard]

I'm now suffering because apparently modern phone browsers think it's a bad idea to let users edit URLs manually :-/

[Kevin Buzzard]

The Star.Matrix file seems to only use unitary groups once, just as a way of saying "I am unitary". In particular it never uses the group structure. So maybe we should have reducible predicates on matrices and endomorphisms saying "I am unitary/symplectic/orthogonal/special linear" and then define all the classical groups as subgroups of general linear groups satisfying these predicates.

[Chris Henson]

As a Lean newcomer who was recently confused by these definitions I very much agree it is more natural to work with subgroups. Just from a practical standpoint having to think about and work around if a "group" is a Subtype or Submonoid is odd. Also, it seems like having consistent Subgroup definitions makes expressing something like special unitary much easier.

[Jireh Loreaux]

The nice thing about docs#Matrix.unitaryGroup is that you automatically get access to all the docs#unitary API (right now there's not a ton, but that's something), and that's already a group.

[Jireh Loreaux]

In any case, I'm agnostic about all this at the moment, so if people have other preferences, that's fine.

[Kevin Buzzard]

The correct solution is one that makes everybody happy and will probably need some thought.

[Ian Allen]

Kevin Buzzard said:

The correct solution is one that makes everybody happy and will probably need some thought.

I almost responded with "does not compute" but realized that you most carefully left out the clause "all of the time".