Commit 2023-09-18 18:26 4575c79c

View on Github →

chore: refactor Lie algebra weight spaces (#7210) 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.

Estimated changes

Modified Mathlib/Algebra/Lie/Nilpotent.lean

deleted theorem LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent

deleted theorem LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent

added theorem LieModule.maxGenEigenSpace_toEndomorphism_eq_top

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.iInf_coe

added theorem LieSubmodule.iInf_coe_toSubmodule

added theorem LieSubmodule.mem_iInf

added theorem LieSubmodule.mem_mk_iff'

Modified Mathlib/Algebra/Lie/Weights.lean

deleted theorem LieModule.coe_weightSpace'

deleted theorem LieModule.exists_preWeightSpace_zero_le_ker_of_isNoetherian

added theorem LieModule.exists_weightSpace_zero_le_ker_of_isNoetherian

added theorem LieModule.lie_mem_maxGenEigenspace_toEndomorphism

deleted theorem LieModule.lie_mem_preWeightSpace_of_mem_preWeightSpace

deleted theorem LieModule.mem_preWeightSpace

added theorem LieModule.mem_weightSpaceOf

deleted def LieModule.preWeightSpace

deleted def LieModule.weightSpace'

added def LieModule.weightSpaceOf