lie_eq_smul_of_mem_rootSpace — Mathlib

English

If x lies in the root space corresponding to α, then [h,x] = α(h) x for all h in H.

Русский

Если x принадлежит корневому пространству, соответствующему α, то для всех h в H выполняется [h, x] = α(h) x.

LaTeX

$$$\forall h \in H:\ [h,x] = \alpha(h)\,x \qquad (x \in \mathrm{rootSpace}(H,\alpha))$$$

Lean4

theorem lie_eq_smul_of_mem_rootSpace {α : H → K} {x : L} (hx : x ∈ rootSpace H α) (h : H) : ⁅h, x⁆ = α h • x :=
  by
  replace hx : x ∈ (ad K L h).maxGenEigenspace (α h) := genWeightSpace_le_genWeightSpaceOf L h α hx
  rw [(isSemisimple_ad_of_mem_isCartanSubalgebra h.property).isFinitelySemisimple.maxGenEigenspace_eq_eigenspace,
    Module.End.mem_eigenspace_iff] at hx
  simpa using hx

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