# Documentation

## Mathlib.RingTheory.MatrixAlgebra

We show Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).

noncomputable def MatrixEquivTensor.toFunBilinear (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) :
A →ₗ[R] Matrix n n R →ₗ[R] Matrix n n A

(Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-bilinear map.

Equations
Instances For
@[simp]
theorem MatrixEquivTensor.toFunBilinear_apply (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) (a : A) (m : Matrix n n R) :
(() a) m = a m.map ()
noncomputable def MatrixEquivTensor.toFunLinear (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) :
TensorProduct R A (Matrix n n R) →ₗ[R] Matrix n n A

(Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-linear map.

Equations
Instances For
noncomputable def MatrixEquivTensor.toFunAlgHom (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] :
TensorProduct R A (Matrix n n R) →ₐ[R] Matrix n n A

The function (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an algebra homomorphism.

Equations
Instances For
@[simp]
theorem MatrixEquivTensor.toFunAlgHom_apply (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (a : A) (m : Matrix n n R) :
() (a ⊗ₜ[R] m) = a m.map ()
noncomputable def MatrixEquivTensor.invFun (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : Matrix n n A) :
TensorProduct R A (Matrix n n R)

(Implementation detail.)

The bare function Matrix n n A → A ⊗[R] Matrix n n R. (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)

Equations
Instances For
@[simp]
theorem MatrixEquivTensor.invFun_zero (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] :
= 0
@[simp]
theorem MatrixEquivTensor.invFun_add (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : Matrix n n A) (N : Matrix n n A) :
@[simp]
theorem MatrixEquivTensor.invFun_smul (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (a : A) (M : Matrix n n A) :
@[simp]
theorem MatrixEquivTensor.invFun_algebraMap (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : Matrix n n R) :
MatrixEquivTensor.invFun R A n (M.map ()) = 1 ⊗ₜ[R] M
theorem MatrixEquivTensor.right_inv (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : Matrix n n A) :
() () = M
theorem MatrixEquivTensor.left_inv (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : TensorProduct R A (Matrix n n R)) :
noncomputable def MatrixEquivTensor.equiv (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] :
TensorProduct R A (Matrix n n R) Matrix n n A

(Implementation detail)

The equivalence, ignoring the algebra structure, (A ⊗[R] Matrix n n R) ≃ Matrix n n A.

Equations
• = { toFun := (), invFun := , left_inv := , right_inv := }
Instances For
noncomputable def matrixEquivTensor (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] :
Matrix n n A ≃ₐ[R] TensorProduct R A (Matrix n n R)

The R-algebra isomorphism Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem matrixEquivTensor_apply (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (M : Matrix n n A) :
() M = Finset.univ.sum fun (p : n × n) => M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1
@[simp]
theorem matrixEquivTensor_apply_std_basis (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (i : n) (j : n) (x : A) :
() () = x ⊗ₜ[R]
@[simp]
theorem matrixEquivTensor_apply_symm (R : Type u) [] (A : Type v) [] [Algebra R A] (n : Type w) [] [] (a : A) (M : Matrix n n R) :
().symm (a ⊗ₜ[R] M) = M.map fun (x : R) => a * () x