rootSpace — Mathlib

English

A variant of the weight-space spanning statement using Weight objects; the supremum over Weight(K L M) weights of genWeightSpace M χ equals ⊤.

Русский

Вариант утверждения: супремум по весовым пространствам над Weight(K L M) даёт полный модуль.

LaTeX

$$$\bigvee_{\chi : \mathrm{Weight}(K,L,M)} \mathrm{genWeightSpace}(M,\chi) = \top$$$

Lean4

/-- Given a nilpotent Lie subalgebra `H ⊆ L`, the root space of a map `χ : H → R` is the weight
space of `L` regarded as a module of `H` via the adjoint action. -/
abbrev rootSpace (χ : H → R) : LieSubmodule R H L :=
  genWeightSpace L χ

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