representations of sl2

Stream: maths

[Matthew Ballard]

Is there a classification of irreps of $\mathfrak{sl}_2$ in mathlib or mathlib adjacent?

[Oliver Nash]

No, but it would be a great addition! All the pieces should be in place.

[Matthew Ballard]

@Matej Penciak

[Matej Penciak]

This sounds really interesting! I'm still really new, so I'm not sure what is/isn't done. What do you think would be the path of least resistance for this proof? Do you think there's enough in place to construct the representations as the graded pieces of differential operators acting on $k[x,y]$?

[Johan Commelin]

I think we should have a dedicated notion of sl2_triple. Because these Lie algebras and their representations play a distinguished role in the further theory. They can certainly be linked to k[x,y] later on, but I don't think that should be the primary definition.

[Damiano Testa]

Also, sl2_triples are very useful for classification results in positive characteristic, so it would be good if there were some part of the theory that worked over at least arbitrary fields, possibly also over ℤ.

[Oliver Nash]

Incidentally if the motivation here is just to add more Lie theory then you could look at https://github.com/leanprover-community/mathlib/projects/14 (Indeed step 0 could be to flesh out /fix up this Project since I spent < 10 minutes putting it together.) There's also lots of other fun Lie-related stuff that could be done (e.g., Coxeter groups, reflection groups would probably be fun and easy).

[Oliver Nash]

If on the other hand, maybe you have an sl2-specific application in mind (Hard Lefschetz theorem anyone?) then ignore the above.

[Yaël Dillies]

@Violeta Hernández is interested in Coxeter groups from the polytope side of the story.

[Oliver Nash]

The classification of the finite Coxeter groups would be fun and useful project and one could generate pretty pictures too.

[Johan Commelin]

one can, but can Lean?

[Oliver Nash]

Sure!