English
There is a LieModule structure on the space of linear maps M →ᴿ N under the action of L, with action defined componentwise by brackets as above.
Русский
Существует структура Ли-модуля на пространстве линейных отображений M →ᴿ N под действием L, задаваемая скобками поэлементно.
LaTeX
$$$\text{LieModule } R\ L\ (M \to_{R} N)$ with bracket action defined by $[x,f](m) = [x,f(m)] - f([x,m])$$$
Lean4
instance instLieModule : LieModule R L (M →ₗ[R] N)
where
smul_lie t x
f := by
ext n
simp only [smul_sub, smul_lie, LinearMap.smul_apply, LieHom.lie_apply, LinearMap.map_smul]
lie_smul t x
f := by
ext n
simp only [smul_sub, LinearMap.smul_apply, LieHom.lie_apply, lie_smul]
