English
For a triangularizable finite-dimensional module, the supremum of genWeightSpace M χ over all χ in Weight K L M equals the whole module.
Русский
Для треугольного конечномерного модуля супремум весовых пространств по всем весам охватывает весь модуль.
LaTeX
$$$\sup_{\chi \in \mathrm{Weight}(K,L,M)} \mathrm{genWeightSpace}(M,\chi) = M$$$
Lean4
/-- For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.
See also `LieModule.iSup_genWeightSpace_eq_top'`. -/
theorem iSup_genWeightSpace_eq_top [IsTriangularizable K L M] : ⨆ χ : L → K, genWeightSpace M χ = ⊤ :=
by
simp only [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule, LieSubmodule.iInf_toSubmodule,
LieSubmodule.top_toSubmodule, genWeightSpace]
refine
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
(fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_
apply IsTriangularizable.maxGenEigenspace_eq_top
