English
For a Lie submodule N of M, IsUcsLimit says there exists a finite step k after which the upper central series stabilizes at N: ⊥.ucs l = N for all l ≥ k.
Русский
Для подмодуля Ли N модуля M условие IsUcsLimit означает, что после некоторого шага k верхняя центральная последовательность стабилизируется на N: ⊥.ucs l = N для всех l ≥ k.
LaTeX
$$$\\exists k, \\forall l\\ge k, (\\perp : LieSubmodule R L M).ucs\\; l = N$$$
Lean4
/-- Given a Lie module `M` of a Lie algebra `L`, `LieSubmodule.IsUcsLimit` is the proposition
that a Lie submodule `N ⊆ M` is the limiting value for the upper central series.
This is a characteristic property of Cartan subalgebras with the roles of `L`, `M`, `N` played by
`H`, `L`, `H`, respectively. See `LieSubalgebra.isCartanSubalgebra_iff_isUcsLimit`. -/
def IsUcsLimit {M : Type*} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
(N : LieSubmodule R L M) : Prop :=
∃ k, ∀ l, k ≤ l → (⊥ : LieSubmodule R L M).ucs l = N
