Special Linear Groups

Stream: Is there code for X?

[Sidharth Hariharan]

Hi all,
I’m a first year undergraduate mathematics student at Imperial College London and a regular attendee at Dr. Kevin Buzzard’s weekly Lean sessions. I am keen to contribute to Mathlib and was browsing through the “Missing undergraduate topics in Lean” page on Lean Community. I found Special Linear Groups on that list, and I couldn’t find it in the Pull Requests either. I was wondering what exactly needs to be done. Any suggestions on how to get started would be much appreciated too.
Thank you!

[Eric Wieser]

It seems we have docs#matrix.special_linear_group but no equivalent definition for linear maps

[Eric Wieser]

I wonder; is docs#unitary applied to docs#module.End distinct from the special linear group?

[Kevin Buzzard]

unitary wants a star, but even if star is trivial you don't get the special linear group, you get orthogonal groups I guess.

[Kevin Buzzard]

@Patrick Massot can Anne's work linked to above be used to remove special linear groups from the UG todo list?

[Eric Wieser]

(docs#linear_map.star_semigroup requires an inner product space too, so is probably too strong on typeclass requirements for docs#unitary to be useful)

[Eric Wieser]

Kevin Buzzard said:

Patrick Massot can Anne's work linked to above be used to remove special linear groups from the UG todo list?

I guess even if we don't want the matrix version, the linear map version is basically just linear_map.det.ker

[Patrick Massot]

I would like to see a version that actually types check.

[Patrick Massot]

I can write

import linear_algebra.determinant

variables {M : Type*} [add_comm_group M] {A : Type*} [comm_ring A] [module A M]

#check @monoid_hom.ker
#check  (linear_map.det : (M →ₗ[A] M) →* A)

but (M →ₗ[A] M) is not a group

[Patrick Massot]

and linear_equiv.det doesn't seem to exist.

[Patrick Massot]

So I would say we don't seem to have the special linear group, but it shouldn't be far away.

[Kevin Buzzard]

@Sidharth Hariharan so it seems that there's a mini project to be done there before we can tick it off -- I can talk you through it next Thurs

[Eric Wieser]

linear_equiv.det doesn't seem to exist

docs#linear_equiv.det

[Eric Wieser]

Apparently I added this in #10751

[Sidharth Hariharan]

@Kevin Buzzard I see. Sounds good, thank you!

[Antoine Labelle]

If we want the linear_map version of the special linear group, it might be good also to add the basis-independant definition of the determinant in terms of exterior powers similar to what we did we the trace recently (docs#linear_map.trace_eq_contract)