[Merged by Bors] - feat(Algebra/Lie/Semisimple): API for semisimple Lie algebras

[jcommelin]

Including the result that ideals in a semisimple Lie algebra
are in a unique way the direct sum of simple ideals.
This result makes no assumptions on the ring of coefficients or the Lie algebra;
it holds over arbitrary base rings, and in arbitrary dimensions.

---

[ocfnash]

This is really nice!

I only have time for some superficial remarks now. My main thought is whether some of the proofs could be golfed by using more of the results about compactly-generated lattices.

I'll have more to say later.

[ocfnash]

Thanks, this is marvelous!

bors d+

[ocfnash]

I can't help wondering if it might be easier to establish modularity instead. So the proof would start:

Suggested change

	constructor
	suffices IsModularLattice α by
	have _i := isAtomistic_of_sSup_eq_top hS h
	apply complementedLattice_of_isAtomistic

More generally I'm not sure what order to establish properties would minimize the effort here (e.g., could we establish complementarity first and then get atomisticness from complementedLattice_iff_isAtomistic etc.).

However what you have is clearly fine.

[jcommelin]

Good suggestion! By putting DistribLattice higher about, I could apply this golf. (It implies modular lattice.)

[mathlib-bors]

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

If you have the appetite I think a nice future refactor would be to remove:

import Mathlib.Algebra.Lie.Solvable

and move all the dependent material (HasTrivialRadical etc.) to its own file.

For bonus points, I think we should also remove this import from Mathlib.Algebra.Lie.Nilpotent and move the two short dependent results into Mathlib.Algebra.Lie.Solvable.

[jcommelin]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style