[Merged by Bors] - feat(Algebra/Lie): add Lie's theorem

[Espio231]

Prove Lie's theorem, that Lie modules of solvable Lie algebras over algebraically closed fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra.

---

[grunweg]

Hello: I'm coming here for issue triage. You marked this PR as help-wanted: can you be more specific what help you need? This makes it easier for other to help you :-)
The lint and build is certainly easy to fix: let me just do this.

[grunweg]

I left a few style comments to get you started (and just pushed the fix to Mathlib.lean, so mathlib's continuous integration can give you feedback).

[grunweg]

Oh, and another comment: did you mean to mark this ready for review? If so, feel free to label it awaiting-review once you have addressed my comments. (I've marked it with awaiting-author now: see this page for an explanation what these labels mean: https://leanprover-community.github.io/contribute/index.html)

[grunweg]

Last, but not least: thank you for your contribution! I'm very happy that mathlib is learning more about Lie groups and Lie algebras and very much look forward to your result landing, once it's ready!

[Espio231]

Thank you very much for the help @grunweg. I marked this as help-wanted since I didn't really understand why continuous integration was failing but you seemed to have fixed this now. I'll get to work on resolving the things you've brought up.

[grunweg]

Thanks for the quick response! I had some time at my hands and decided to leave a few more comments, mostly about coding style. (This covers perhaps the first half of your PR.)

[grunweg]

By the way: once you have dealt with a comment, feel free to mark it as "resolved" in Github. This way, I and future reviews can see which points are still open or not. If you're not sure, leaving it open is fine (but in practice, for many suggestions it's clear once they were resolved).

[github-actions]

PR summary 02441991c7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Lie.LieTheorem (new file)	1472

---

Declarations diff

+ exists_nontrivial_weightSpace_of_isNilpotent
+ exists_nontrivial_weightSpace_of_isSolvable
+ exists_nontrivial_weightSpace_of_lieIdeal
+ instance : CanLift (Submodule R M) (LieSubmodule R L M) (·)
+ weightSpaceOfIsLieTower

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jcommelin]

There already is an api for turning complementary submodules into a direct sum. With my current suggestion, you can remove your pr1 and pr2 declarations.

You may also want to assume IsCompl in more places, instead of separe (Co)Disjoint hypotheses.

[ocfnash]

Thanks for this, it looks very nearly ready now.

[ocfnash]

I thought a little about this again this morning and I think it might be worth defining a new type BiLieSubmodule (which could go in a new file, naming TBD) and using it to develop things as follows:

variable (R L₁ L₂ M : Type*)
  [CommRing R] [AddCommGroup M] [Module R M]
  [LieRing L₁] [LieAlgebra R L₁] [LieRingModule L₁ M] [LieModule R L₁ M]
  [LieRing L₂] [LieAlgebra R L₂] [LieRingModule L₂ M] [LieModule R L₂ M]

/-- Naming TBD -/
structure BiLieSubmodule extends Submodule R M where
  lie_mem_left : ∀ {x : L₁} {m : M}, m ∈ carrier → ⁅x, m⁆ ∈ carrier
  lie_mem_right : ∀ {x : L₂} {m : M}, m ∈ carrier → ⁅x, m⁆ ∈ carrier

def LieSubmodule.toBiLieSubmodule_of_lieIdeal_left (N : LieSubmodule R L₁ M) (I : LieIdeal R L₁) :
    BiLieSubmodule R I L₁ M :=
  { toSubmodule := N
    lie_mem_left := LieSubmodule.lie_mem _
    lie_mem_right := LieSubmodule.lie_mem _ }

-- Bit more API for BiLieSubmodule, including coercions to `LieSubmodule R Lᵢ M` etc

/-- The non-trivial result justifying the `BiLieSubmodule` concept. -/
def biWeightSpaceLeft [IsPrincipalIdealRing R] [IsDomain R] [CharZero R]
    [Module.Free R M] [Module.Finite R M]
    [Bracket L₁ L₂] [Bracket L₂ L₁] [IsLieTower L₁ L₂ M] [IsLieTower L₂ L₁ M]
    (χ : L₁ → R) :
    BiLieSubmodule R L₁ L₂ M :=
  { toSubmodule := weightSpace M χ
    lie_mem_left := LieSubmodule.lie_mem _
    lie_mem_right x {m} hm := lie_stable χ x m hm /- modulo renaming of `lie_stable` -/ }

[ocfnash]

Another passing thought is that maybe this BiLieSubmodule idea is silly and what we really have is LieSubmodule R (L₁ × L₂) M. I just tried to check this in Lean and annoyingly we don't have the basic theory of binary products of Lie algebras (and their representations). On paper the calculation also didn't work out but I feel like this is still worth some thought. Unfortunately I probably won't have time.

I also don't think it is necessary to use my various suggestions from this morning. Clearly things are in reasonable shape; it's just that I'd like to feel like I understand the true content of Lie's theorem.

[jcommelin]

it's just that I'd like to feel like I understand the true content of Lie's theorem.

This resonates with me a lot. I still feel like I haven't found the ultimate proof. But after many iterations, I'm out of ideas for finding a better version than the current one.

[ocfnash]

Thanks so much for all this work both @Espio231 for the original result and @jcommelin for a heroic effort getting it ready for Mathlib!

Apart from minor naming issues (for which I think I am responsible 🤦 ) I think this is ready to go.

If I get time in the weeks ahead, I may try to find some other points of view since although I follow the argument, I don't really feel I understand the true content.

Anyway, this is great.

bors d+

[mathlib-bors]

✌️ Espio231 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]

bors d=@jcommelin

[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.

[jcommelin]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style