weightSpaceOfIsLieTower — Mathlib

English

For χ : A → R, the weight space of V with respect to χ is a Lie submodule for L (i.e., closed under the action of L).

Русский

Пусть χ: A → R. Весовое пространство V по χ является подмодулем Ли для действия L (то есть замкнуто относительно [L, ·]).

LaTeX

$$$\\forall z \\in L,\\; \\forall v \\in \\operatorname{weightSpace}(V,\\chi),\\ [z,v] \\in \\operatorname{weightSpace}(V,\\chi).$$$

Lean4

/-- The weight space of `V` with respect to `χ : A → R`, a priori a Lie submodule for `A`, is also a
Lie submodule for `L`. -/
def weightSpaceOfIsLieTower (χ : A → R) : LieSubmodule R L V :=
  { toSubmodule := weightSpace V χ
    lie_mem {z v} hv := weightSpaceOfIsLieTower_aux χ z v hv }

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