Leiden representation theory project

Stream: general

[Daan van Gent]

Hi all,

@Jesse Vogel and I organize an informal Lean workshop in Leiden for PhD students and up.
The first phase of this workshop, teaching everyone the basics, is coming to an end, and we plan to start phase two soon, where with a smaller group (6ish) we plan to contribute to mathlib.

Having checked the todos, I was thinking to go for representation theory, in the direction of Burnside's theorem on solvable groups.
It seemed like a good idea to sanity check this idea with the comunity, and also get in touch with the people working on the representation theory in Lean.
I hope it is not considered rude to @ some recent contributors on github (@Amelia Livingston, @Anne Baanen, @Antoine Labelle, @Eric Rodriguez).

Our rough plan would be to split up in two teams, one writing theorems with sorry's, and one replacing sorry's with proofs.
I think we will follow HW Lenstra's lecture notes, but maybe we will find a better source.
At least two people on our team have contributed to mathlib before, so I expect the git experience to go relatively smoothly.

Best,
Daan

[Scott Morrison]

This has stalled while I work on other things, but I started a tutorial based on Etingof's representation theory notes, at https://github.com/leanprover-community/mathlib/pull/13911, which some may find helpful/inspiring/adoptable. :-)

[Antoine Labelle]

Glad to see more people interested in representation theory in Lean!

[Julian Külshammer]

I'm also interested in representation theory (my expertise is more towards representation theory of finite-dimensional algebras though, and recently I haven't had much time for Lean unfortunately). Do you think it would make sense to create a representation theory stream on Zulip or do you have some separate communication platform?

[Kevin Buzzard]

When Galois theory was being developed there was a separate public stream which was mostly just questions and answers from the Berkeley crowd who were developing it (Galois theory was also developed by a small group who were physically in one place) and I thought it worked really well. I would read the stream but those not interested in Galois theory could just mute it

[Daan van Gent]

Scott Morrison said:

This has stalled while I work on other things, but I started a tutorial based on Etingof's representation theory notes, at https://github.com/leanprover-community/mathlib/pull/13911, which some may find helpful/inspiring/adoptable. :-)

Thanks, we will check it out!

Kevin Buzzard said:

When Galois theory was being developed there was a separate public stream which was mostly just questions and answers from the Berkeley crowd who were developing it (Galois theory was also developed by a small group who were physically in one place) and I thought it worked really well. I would read the stream but those not interested in Galois theory could just mute it

We do not have any method of communicating other than in person meet-ups, so a stream here might be a good idea. I am not sure if I have the rights to create one.

[Johan Commelin]

@Daan van Gent I'll create one for you