hasBracket — Mathlib

English

For a Lie module M over L and Lie submodule N, the bracket [I,N] is the Lie-submodule generated by all brackets [x,n] with x ∈ I and n ∈ N, where I is a Lie ideal of L.

Русский

Для Ли-модуля M над Ли-алгеброй L и подмодуля N, скобка [I,N] является порождённым Ли-подмодулем всеми скобками [x,n], где x ∈ I и n ∈ N, где I — Ли-идеал L.

LaTeX

$$$$ [I,N] = \operatorname{lieSpan}_R^L\{ [x,n] \mid x \in I, n \in N \}. $$$$

Lean4

/-- Given a Lie module `M` over a Lie algebra `L`, the set of Lie ideals of `L` acts on the set
of submodules of `M`. -/
instance hasBracket : Bracket (LieIdeal R L) (LieSubmodule R L M) :=
  ⟨fun I N => lieSpan R L {⁅(x : L), (n : M)⁆ | (x : I) (n : N)}⟩

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