English
The natural equivalence between linear endomorphisms of a finite free module and square matrices is a Lie algebra isomorphism.
Русский
Естественное глобальное тождество между линейными отображениями на конечном свободном модуле и квадратными матрицами является изоморфизмом по Ли‑алгебрам.
LaTeX
$$$ \\operatorname{End}_R(R^n) \\cong_{\\mathfrak{lie}} \\operatorname{Mat}_{n\\times n}(R). $$$
Lean4
/-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
is compatible with the Lie algebra structures. -/
def lieEquivMatrix' : Module.End R (n → R) ≃ₗ⁅R⁆ Matrix n n R :=
{ LinearMap.toMatrix' with
map_lie' := fun {T S} => by
let f := @LinearMap.toMatrix' R _ n n _ _
change f (T.comp S - S.comp T) = f T * f S - f S * f T
have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
rw [map_sub, h, h] }
