English
For LieIdeal I ⊆ L and LieSubmodule N ⊆ M, the Lie bracket [I,N] equals the range of the composed map toModuleHom ∘ mapIncl: I ⊗R N → L ⊗R M → M.
Русский
Пусть I ⊆ L — Ли-идеал, N ⊆ M — Ли-подмодуль. Брэкет [I,N] равен образу композиции toModuleHom ∘ mapIncl: I ⊗N → L ⊗M → M.
LaTeX
$$$$ [I,N] = \operatorname{range}\big( (toModuleHom\;R\;L\;M) \circ (mapIncl\; I\; N) \big). $$$$
Lean4
/-- The action of the Lie algebra on one of its modules, regarded as a morphism of Lie modules. -/
def toModuleHom : L ⊗[R] M →ₗ⁅R,L⁆ M :=
TensorProduct.LieModule.liftLie R L L M M
{ (toEnd R L M : L →ₗ[R] M →ₗ[R] M) with
map_lie' := fun {x m} => by ext n; simp [LieRing.of_associative_ring_bracket] }
