English
The composite product on root spaces and weight spaces gives a Lie algebra homomorphism from the tensor product of root spaces and weight spaces to the weight space with the sum of weights.
Русский
Композитное произведение между корневым пространством и весовым пространством задаёт гомоморфизм Ли из тензорного произведения в весовое пространство с суммой весов.
LaTeX
$$$\mathrm{rootSpaceWeightSpaceProduct} : \mathrm{rootSpace} H χ_1 ⊗ \mathrm{genWeightSpace} M χ_2 →\mathrm{genWeightSpace} M (χ_1+χ_2)$$$
Lean4
theorem rootSpaceProduct_tmul (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : rootSpace H χ₁) (y : rootSpace H χ₂) :
(rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ (x ⊗ₜ y) : L) = ⁅(x : L), (y : L)⁆ := by
simp only [rootSpaceProduct_def, coe_rootSpaceWeightSpaceProduct_tmul]
