English
For a nilpotent Lie algebra L acting on M, the posFittingComp is defined as the supremum (over x ∈ L) of the positive Fitting components posFittingCompOf(R,M,x).
Русский
Для нильпотентной Ли-алгебры L, действующей на M, posFittingComp определяется как супремум положительных компонент Фиттинга posFittingCompOf(R,M,x) по x∈L.
LaTeX
$$$\operatorname{posFittingComp}(R,L,M) = \bigvee_{x\in L} \operatorname{posFittingCompOf}(R,M,x)$$$
Lean4
/-- If `M` is a representation of a nilpotent Lie algebra `L` with coefficients in `R`, then
`posFittingComp R L M` is the span of the positive Fitting components of the action of `x` on `M`,
as `x` ranges over `L`.
It is a Lie submodule because `L` is nilpotent. -/
def posFittingComp : LieSubmodule R L M :=
⨆ x, posFittingCompOf R M x
