Discussion: low-dim solvable Lie algebras

Stream: general

[Oliver Nash]

Discussion thread for #announce > Classification results for Lie algebras

@Paul Schwahn Congratulations! Also, I'm delighted to see someone using the Lie theory. My immediate remarks are:

• please consider upstreaming as much as possible to Mathlib
• please consider joining in on the (semi)simple version: https://github.com/ocfnash/LieClassification/

Nice work!

[Kevin Buzzard]

As a general tip, mathlib won't accept non-terminal simps so please replace them with simp? and then the corresponding simp only call (or even better, see what the output of simp only is and then rearrange the proof so that simp is used to close the goal).

[Paul Schwahn]

Thanks, Oliver! Yes, in fact our immediate next goal is to make some pull requests to mathlib. I've also posted about it here: #maths > Low-dimensional Lie algebras @ 💬
(because I don't know what the appropriate channel to discuss it is). As mentioned there, we have already converged on a theorem for our first pull request, and we will (slowly) start preparing it now.

I'd also be willing to join your project on semisimple Lie algebras at some point! Although I can't yet promise when that will be, because of other obligations.

[Johan Commelin]

@Paul Schwahn #maths > Low-dimensional Lie algebras is certainly appropriate! And this thread as well.

We try to keep #announce low-traffic, because many people are subscribed to it. That's why we have discussion threads in for announcement posts in a different channel.

[Yaël Dillies]

The issue I think is that you didn't mark #maths > Low-dimensional Lie algebras as the discussion thread corresponding to your announcement. Had you done, Olived wouldn't have created a new one

[Paul Schwahn]

To start getting the hang of it, we have prepared our first pull request, #26126, which just contains the theorem LieIdeal.comap_incl_eq_bot, an analogue (for Lie ideals and Lie algebra homomorphisms) to the already existing theorem LieSubmodule.comap_incl_eq_bot (for Lie submodules and Lie module homomorphisms). Many more will follow. Reviews are appreciated!