English
If x lies in the root space with weight χ1 and m lies in the weight space for χ2, then the Lie bracket [x,m] lies in the weight space for χ1+χ2.
Русский
Если x в корневом пространстве веса χ1, а m в весовом пространстве χ2, то [x,m] принадлежит весовому пространству χ1+χ2.
LaTeX
$$$\{x,m\}$ с $x \in \mathrm{rootSpace} H χ_1$, $m \in \mathrm{genWeightSpace} M χ_2$ imply \[x,m\] \in \mathrm{genWeightSpace} M (χ_1+χ_2)$$$
Lean4
theorem lie_mem_genWeightSpace_of_mem_genWeightSpace {χ₁ χ₂ : H → R} {x : L} {m : M} (hx : x ∈ rootSpace H χ₁)
(hm : m ∈ genWeightSpace M χ₂) : ⁅x, m⁆ ∈ genWeightSpace M (χ₁ + χ₂) :=
by
rw [genWeightSpace, LieSubmodule.mem_iInf]
intro y
replace hx : x ∈ genWeightSpaceOf L (χ₁ y) y := by rw [rootSpace, genWeightSpace, LieSubmodule.mem_iInf] at hx;
exact hx y
replace hm : m ∈ genWeightSpaceOf M (χ₂ y) y := by rw [genWeightSpace, LieSubmodule.mem_iInf] at hm; exact hm y
exact lie_mem_maxGenEigenspace_toEnd hx hm
