English
Let R be a commutative ring, L a nilpotent Lie algebra over R, and M an additive group with an R-module structure and a compatible Lie action by L, with NoZeroSmulDivisors on R acting on M and M being Noetherian. Then the collection of weights Weight(R,L,M) is finite.
Русский
Пусть R — коммутативный кольцо, L — нильпотентная Ли-алгебра над R, а M — аддитивная группа с структурой R-модуля и совместным действием L на M. Пусть нет нулевых делителей и M конечно порождено. Тогда множество весов Weight(R,L,M) конечно.
LaTeX
$$$\#\mathrm{Weight}(R,L,M) < \infty$$$
Lean4
instance instFinite [NoZeroSMulDivisors R M] [IsNoetherian R M] : Finite (Weight R L M) :=
by
have : Finite {χ : L → R | genWeightSpace M χ ≠ ⊥} := finite_genWeightSpace_ne_bot R L M
exact Finite.of_injective (equivSetOf R L M) (equivSetOf R L M).injective
