English
For a LieSubalgebra K ⊆ L, the endomorphism acting on K agrees with the endomorphism acting on L when restricted to K.
Русский
Для подалгебры K ⊆ L действия на K совпадают с действиями на L при ограничении к K.
LaTeX
$$$$\text{toEnd}_R(K,M)\big|_{K} = \text{toEnd}_R(L,M)\Big|_{K}.$$$$
Lean4
/-- A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.
See also `LieModule.toModuleHom`. -/
@[simps]
def toEnd : L →ₗ⁅R⁆ Module.End R M
where
toFun
x :=
{ toFun := fun m => ⁅x, m⁆
map_add' := lie_add x
map_smul' := fun t => lie_smul t x }
map_add' x y := by ext m; apply add_lie
map_smul' t x := by ext m; apply smul_lie
map_lie' {x y} := by ext m; apply lie_lie
