Commit 2023-11-14 15:34 87c833e0

View on Github →

feat: weight space decomposition of Lie modules (#7963)

Estimated changes

Modified Mathlib/Algebra/Lie/CartanSubalgebra.lean

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem LieSubmodule.mapsTo_pow_toEndomorphism_sub_algebraMap

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.codisjoint_iff_coe_toSubmodule

added theorem LieSubmodule.coeSubmodule_eq_bot_iff

added theorem LieSubmodule.coeSubmodule_eq_top_iff

added theorem LieSubmodule.disjoint_iff_coe_toSubmodule

added theorem LieSubmodule.injective_incl

added theorem LieSubmodule.isCompactElement_lieSpan_singleton

modified theorem LieSubmodule.map_iSup

added theorem LieSubmodule.sSup_image_lieSpan_singleton

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

modified theorem LieModule.comap_weightSpace_eq_of_injective

added theorem LieModule.disjoint_weightSpace

added theorem LieModule.disjoint_weightSpaceOf

added theorem LieModule.iSup_weightSpaceOf_eq_top

added theorem LieModule.iSup_weightSpace_eq_top

added theorem LieModule.independent_weightSpace

added theorem LieModule.injOn_weightSpace

modified theorem LieModule.map_weightSpace_eq_of_injective

added theorem LieModule.weightSpace_le_weightSpaceOf

added theorem LieModule.weightSpace_weightSpaceOf_map_incl