English
The generalized weight space genWeightSpace is defined as the infimum over x ∈ L of genWeightSpaceOf M (χ x) x; i.e., it is the intersection of all maximal generalized χ x-eigenspaces coming from all x ∈ L.
Русский
Обобщенное весовое пространство genWeightSpace задаётся как Infimum по x ∈ L: genWeightSpace M χ = ∩_{x∈L} genWeightSpaceOf M (χ x) x.
LaTeX
$$$\\mathrm{genWeightSpace}(M, χ) = \\bigwedge_{x \\in L} \\mathrm{genWeightSpaceOf}(M, χ(x), x)$$$
Lean4
/-- If `M` is a representation of a nilpotent Lie algebra `L`
and `χ : L → R` is a family of scalars,
then `genWeightSpace M χ` is the intersection of the maximal generalized `χ x`-eigenspaces
of the action of `x` on `M` as `x` ranges over `L`.
It is a Lie submodule because `L` is nilpotent. -/
def genWeightSpace (χ : L → R) : LieSubmodule R L M :=
⨅ x, genWeightSpaceOf M (χ x) x
