coe_rootSpaceWeightSpaceProduct_tmul

English

For χ and α weights, the map given by x in rootSpace H α induces a map sending genWeightSpace M χ into genWeightSpace M (α+χ).

Русский

Для весов χ и α отображение, заданное x из корневого пространства H α, переводит genWeightSpace M χ в genWeightSpace M (α+χ).

LaTeX

$$$\text{MapsTo}\; (\mathrm{toEnd}\; R L M x)\; \mathrm{genWeightSpace}(M,χ) \; \mathrm{genWeightSpace}(M,α+χ)$$$

Lean4

@[simp]
theorem coe_rootSpaceWeightSpaceProduct_tmul (χ₁ χ₂ χ₃ : H → R) (hχ : χ₁ + χ₂ = χ₃) (x : rootSpace H χ₁)
    (m : genWeightSpace M χ₂) : (rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ (x ⊗ₜ m) : M) = ⁅(x : L), (m : M)⁆ :=
  by
  simp only [rootSpaceWeightSpaceProduct, rootSpaceWeightSpaceProductAux, coe_liftLie_eq_lift_coe, lift_apply,
    LinearMap.coe_mk, AddHom.coe_mk, Submodule.coe_mk]

Похожие утверждения