English
If M is a representation of a Lie algebra L and χ: L → R is a weight function, then the weight space weightSpace(M, χ) consists of vectors m ∈ M such that for every x ∈ L, [x,m] = χ(x) m. Equivalently, it is the intersection of the χ(x)-eigenspaces for the action of x on M.
Русский
Если M — представление Lie-алгебры L и χ: L → R — весовая функция, то весовое пространство weightSpace(M, χ) состоит из векторов m ∈ M таких, что для каждого x ∈ L выполняется [x, m] = χ(x) m. Иными словами, это пересечение χ(x)-собственных пространств действия x на M.
LaTeX
$$$\\mathrm{weightSpace}(M, \\chi) = \\bigcap_{x \\in L} \\{ m \\in M : [x,m] = \\chi(x) m \\}$$$
Lean4
/-- If `M` is a representation of a Lie algebra `L` and `χ : L → R` is a family of scalars,
then `weightSpace M χ` is the intersection of the `χ x`-eigenspaces
of the action of `x` on `M` as `x` ranges over `L`. -/
def weightSpace (χ : L → R) : LieSubmodule R L M
where
__ := ⨅ x : L, (toEnd R L M x).eigenspace (χ x)
lie_mem {x m} hm := by simp_all [smul_comm (χ x)]
