English
For a linear map f: M →ᴿ N, the bracket with x ∈ L acts by ([x,f])(m) = [x, f(m)] − f([x,m]).
Русский
Для линейного отображения f: M →ᴿ N скобка с x ∈ L действует так: ([x,f])(m) = [x, f(m)] − f([x,m]).
LaTeX
$$$[x, f] (m) = [x, f(m)] - f([x,m])$$$
Lean4
instance instLieRingModule : LieRingModule L (M →ₗ[R] N)
where
bracket x
f :=
{ toFun := fun m => ⁅x, f m⁆ - f ⁅x, m⁆
map_add' := fun m n => by
simp only [lie_add, LinearMap.map_add]
abel
map_smul' := fun t m => by simp only [smul_sub, LinearMap.map_smul, lie_smul, RingHom.id_apply] }
add_lie x y
f := by
ext n
simp only [add_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply, LinearMap.map_add]
abel
lie_add x f
g := by
ext n
simp only [LinearMap.coe_mk, AddHom.coe_mk, lie_add, LinearMap.add_apply]
abel
leibniz_lie x y
f := by
ext n
simp only [lie_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.map_sub, LinearMap.add_apply, lie_sub]
abel
