[Merged by Bors] - feat(algebra/lie/basic): nilpotent and solvable Lie algebras #5382
Conversation
| @@ -564,8 +564,7 @@ instance lie_subalgebra_lie_ring (L' : lie_subalgebra R L) : lie_ring L' := | |||
| leibniz_lie := by { intros, apply set_coe.ext, apply leibniz_lie, } } | |||
|
|
|||
| /-- A Lie subalgebra forms a new Lie algebra. -/ | |||
| instance lie_subalgebra_lie_algebra (L' : lie_subalgebra R L) : | |||
| @lie_algebra R L' _ (lie_subalgebra_lie_ring _ _ _) := | |||
| instance lie_subalgebra_lie_algebra (L' : lie_subalgebra R L) : lie_algebra R L' := | |||
There was a problem hiding this comment.
This is a totally unrelated change that I just noticed.
|
|
||
| /-- The derived Lie submodule of a Lie module. -/ | ||
| def derived_lie_submodule : lie_submodule R L M := ⁅(⊤ : lie_ideal R L), ⊤⁆ |
There was a problem hiding this comment.
Evidently I am proposing to drop this definition (even though I only just introduced it!). This is because:
- The name is not really right: there is no derived series for a Lie module. If anything this should be the "lower central submodule".
- We don't need it since we should have the
derived_seriesandlower_central_serieswith these changes.
ocfnash
added
the
awaiting-review
There was a problem hiding this comment.
This is looking good. But would you mind adding some stuff around these definitions?
For example:
- in an abelian lie algebra, the bracket of any two ideals is
0. - hence abelian lie algebras are nilpotent.
- N is nilpotent <=> \exists sequence of submodules N_i, such that [L, N_i] sub N_{i+1}, and N_0 = N, and N_i = 0 for large enough i.
- L is solvable <=> \exists sequence of ideal L_i, such that [L_i, L_i] sub L_{i+1}, and L_0 = L, and L_i = 0 for large enough i.
- hence L nilpotent implies L solvable
My hope/guess is that this might actually be not too unpleasant to formalise.
Thanks, I'd be happy to do as you suggest. I have some time this evening so let's see how far I can get.
Likewise, especially on the hoping bit! |
Note that this means we thus have: ```lean example [is_lie_abelian L] : ⁅I, J⁆ = ⊥ := by simp ```
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
|
@jcommelin I think I'm out of juice for today. Thanks for all the help. I note that two of your suggestions are still pending. I hope to pick this up tomorrow. |
|
@ocfnash maybe this is fine for the current PR. the other two points could be combined with things like: injective map from L to nilp/solv Lie algebra means that L is nilp/solv, and similarly surjective map from nilp/solv to L means that L is nilp/solv. |
github-actions
bot
added
ready-to-merge
bryangingechen
changed the title
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
An alternative proposal to my original #5241 (which I will close if we opt to merge these changes)