English
Let f: α →ₐ[R] β be an algebra homomorphism. Then the induced map on matrices maps each entry by f, giving an algebra homomorphism between matrix algebras.
Русский
Пусть f: α →ₐ[R] β — алгебраическое гомоморфизм. Тогда индуцированное отображение на матрицах по каждому элементу задаёт гомоморфизм между соответствующими матричными алгебрами.
LaTeX
$$$[(\mathrm{mapMatrix}\ f)(M)]_{ij} = f(M_{ij})$ for all i,j.$$
Lean4
/-- The `AlgHom` between spaces of square matrices induced by an `AlgHom` between their
coefficients. This is `Matrix.map` as an `AlgHom`. -/
@[simps]
def mapMatrix (f : α →ₐ[R] β) : Matrix m m α →ₐ[R] Matrix m m β :=
{ f.toRingHom.mapMatrix with
toFun := fun M => M.map f
commutes' := fun r => Matrix.map_algebraMap r f (map_zero _) (f.commutes r) }
