English
Auxiliary bilinear map taking a root vector x and a weight vector m to a weight-space element in a higher weight χ1+χ2, defined via a lifted Lie bracket.
Русский
Вспомогательное билинейное отображение, которое берет корневой вектор x и весовой вектор m и возвращает элемент весового пространства в более высокой весовой степени χ1+χ2, заданное через поднятую скобку Ли.
LaTeX
$$$\text{def }\mathrm{rootSpaceWeightSpaceProductAux} (χ_1,χ_2,χ_3) (hχ : χ_1+χ_2=χ_3) : \mathrm{rootSpace} H χ_1 →\cdot genWeightSpace M χ_2 →\cdot genWeightSpace M χ_3$$$
Lean4
theorem toEnd_pow_apply_mem {χ₁ χ₂ : H → R} {x : L} {m : M} (hx : x ∈ rootSpace H χ₁) (hm : m ∈ genWeightSpace M χ₂)
(n) : (toEnd R L M x ^ n : Module.End R M) m ∈ genWeightSpace M (n • χ₁ + χ₂) := by
induction n with
| zero => simpa using hm
| succ n IH =>
simp only [pow_succ', Module.End.mul_apply, toEnd_apply_apply]
convert lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
rw [succ_nsmul, ← add_assoc, add_comm (n • _)]
