[Merged by Bors] - chore: refactor Lie algebra weight spaces #7210
Conversation
The key change is the new definition `LieModule.weightSpaceOf` which shows that the eigenspaces of the action of a single element of a Lie algebra on a representation are Lie submodules. I need to use this fact to develop the theory further.
ocfnash
added
awaiting-review
awaiting-CI
t-algebra
| exact LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent R L } | ||
| #align lie_module.weight_space LieModule.weightSpace | ||
| exact lie_mem_maxGenEigenspace_toEndomorphism (by simp) hm } | ||
|
|
There was a problem hiding this comment.
Would it be possible to change the meaning of 𝕎 M χ x, so that it now denotes a weight space? Or do you think that's not a good idea?
There was a problem hiding this comment.
I'd be very reluctant to have the same notation mean different things in this way.
I claim the notation for (toEndomorphism R L M x).maximalGeneralizedEigenspace χ is useful because it's such a mouthful and we will never care about it (in statements anyway) once we define weightSpaceOf M χ x.
However I think weightSpace M χ is perfectly fine and not in need of notation.
Of course I'm open to suggestions but as I say, I'd be reluctant to overload notation depending on context.
There was a problem hiding this comment.
Fair enough, makes a lot of sense
jcommelin
added
awaiting-author
ocfnash
added
awaiting-review
and removed
awaiting-author
leanprover-community-mathlib4-bot
added
ready-to-merge
The key change is the new definition `LieModule.weightSpaceOf` which shows that the eigenspaces of the action of a single element of a Lie algebra on a representation are Lie submodules. I need to use this fact to develop the theory further.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
The key change is the new definition `LieModule.weightSpaceOf` which shows that the eigenspaces of the action of a single element of a Lie algebra on a representation are Lie submodules. I need to use this fact to develop the theory further.
The key change is the new definition
LieModule.weightSpaceOfwhich shows that the eigenspaces of the action of a single element of a Lie algebra on a representation are Lie submodules. I need to use this fact to develop the theory further.