Zulip Chat Archive

Stream: maths

Topic: (Group action of) SL(n) in mathlib


view this post on Zulip Anne Baanen (Dec 05 2019 at 14:59):

Hi! I want to take quotients modulo the action of SL(n) on some structure, but I can't find anything about SL(n) or matrix inverses in mathlib. Am I overlooking something, or is this missing from mathlib?

view this post on Zulip Anne Baanen (Dec 05 2019 at 15:02):

@Rob Lewis just said in person that it is indeed not formalized yet. Follow-up question: what would be the best way to define inverses?

view this post on Zulip Anne Baanen (Dec 05 2019 at 15:06):

Since mathlib typically defines partial operations by defining a total function and assuming the relevant preconditions in the theorems about this operation, my guess would be to start with pseudoinverses and then show that these are true inverses if the determinant is invertible, right?

view this post on Zulip Chris Hughes (Dec 05 2019 at 15:09):

I think there are a lot of different types of pseudoinverse. It would be desirable for the inverse function to return a left inverse if it exists and a right inverse if it exists for rectangular matrices.

view this post on Zulip Anne Baanen (Dec 05 2019 at 15:13):

The pseudoinverse I was thinking of is apparently called the Moore-Penrose inverse. IIRC, it is also the left or right inverse if only one of them exists.


Last updated: May 06 2021 at 19:30 UTC