English
Let M be a module over a commutative semiring R with a finite basis indexed by a finite type n. Then the R-algebra of endomorphisms End_R(M) is canonically isomorphic to the algebra of n-by-n matrices over R; the isomorphism is given by expressing each endomorphism in the basis as a matrix.
Русский
Пусть M — модуль над R с конечным базисом, индексированным множеством n. Тогда алгебра End_R(M) изоморфна алгебре матриц размером n×n над R; изomорфизм даётся выражением каждого эндоморфизма в базисе как матрицы.
LaTeX
$$$\\operatorname{End}_R(M) \\cong_R \\mathrm{M}_n(R)$$$
Lean4
/-- A basis of a module induces an equivalence of algebras from the endomorphisms of the module to
square matrices. -/
def algEquivMatrix [Fintype n] (h : Basis n R M) : Module.End R M ≃ₐ[R] Matrix n n R :=
(h.equivFun.algConj R).trans algEquivMatrix'
