English
An AlgEquiv f: α ≃ₐ[R] β induces an AlgEquiv between matrix algebras: mapMatrix(f): Matrix m m α ≃ₐ[R] Matrix m m β, acting entrywise.
Русский
Алгебраическое эквинвариантное отображение f: α ≃ₐ[R] β порождает эквивариант между матричными алгебрами: mapMatrix(f): Mat_{m×m}(α) ≃ₐ[R] Mat_{m×m}(β), действующее по элементам.
LaTeX
$$$\text{mapMatrix}(f) : \mathrm{Mat}_{m\times m}(\alpha) \simeq_{\text{Alg}} \mathrm{Mat}_{m\times m}(\beta), \; [\text{mapMatrix}(f)(M)]_{ij} = f(M_{ij}).$$$
Lean4
/-- The `AlgEquiv` between spaces of square matrices induced by an `AlgEquiv` between their
coefficients. This is `Matrix.map` as an `AlgEquiv`. -/
@[simps apply]
def mapMatrix (f : α ≃ₐ[R] β) : Matrix m m α ≃ₐ[R] Matrix m m β :=
{ f.toAlgHom.mapMatrix,
f.toRingEquiv.mapMatrix with
toFun := fun M => M.map f
invFun := fun M => M.map f.symm }
