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

noncomputable def MatrixEquivTensor.toFunBilinear (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] : 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

• MatrixEquivTensor.toFunBilinear n R A = (Algebra.lsmul R R (Matrix n n A)).toLinearMap.compl₂ (Algebra.linearMap R A).mapMatrix

@[simp]

theorem MatrixEquivTensor.toFunBilinear_apply (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (m : Matrix n n R) : ((toFunBilinear n R A) a) m = a • m.map ⇑(algebraMap R A)

noncomputable def MatrixEquivTensor.toFunLinear (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] : 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

• MatrixEquivTensor.toFunLinear n R A = TensorProduct.lift (MatrixEquivTensor.toFunBilinear n R A)

noncomputable def MatrixEquivTensor.toFunAlgHom (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] : 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

• MatrixEquivTensor.toFunAlgHom n R A = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (MatrixEquivTensor.toFunLinear n R A) ⋯ ⋯

@[simp]

theorem MatrixEquivTensor.toFunAlgHom_apply (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (a : A) (m : Matrix n n R) : (toFunAlgHom n R A) (a ⊗ₜ[R] m) = a • m.map ⇑(algebraMap R A)

noncomputable def MatrixEquivTensor.invFun (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (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

• MatrixEquivTensor.invFun n R A M = ∑ p : n × n, M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1

@[simp]

theorem MatrixEquivTensor.invFun_zero (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] : invFun n R A 0 = 0

@[simp]

theorem MatrixEquivTensor.invFun_add (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M N : Matrix n n A) : invFun n R A (M + N) = invFun n R A M + invFun n R A N

@[simp]

theorem MatrixEquivTensor.invFun_smul (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (a : A) (M : Matrix n n A) : invFun n R A (a • M) = a ⊗ₜ[R] 1 * invFun n R A M

@[simp]

theorem MatrixEquivTensor.invFun_algebraMap (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n R) : invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M

theorem MatrixEquivTensor.right_inv (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n A) : (toFunAlgHom n R A) (invFun n R A M) = M

theorem MatrixEquivTensor.left_inv (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : TensorProduct R A (Matrix n n R)) : invFun n R A ((toFunAlgHom n R A) M) = M

noncomputable def MatrixEquivTensor.equiv (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] : 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

• MatrixEquivTensor.equiv n R A = { toFun := ⇑(MatrixEquivTensor.toFunAlgHom n R A), invFun := MatrixEquivTensor.invFun n R A, left_inv := ⋯, right_inv := ⋯ }

noncomputable def matrixEquivTensor (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] : 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.

@[simp]

theorem matrixEquivTensor_apply (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (M : Matrix n n A) : (matrixEquivTensor n R A) M = ∑ p : n × n, M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1

@[simp]

theorem matrixEquivTensor_apply_stdBasisMatrix (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (i j : n) (x : A) : (matrixEquivTensor n R A) (Matrix.stdBasisMatrix i j x) = x ⊗ₜ[R] Matrix.stdBasisMatrix i j 1

@[deprecated matrixEquivTensor_apply_stdBasisMatrix (since := "2024-08-11")]

theorem matrixEquivTensor_apply_std_basis (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (i j : n) (x : A) : (matrixEquivTensor n R A) (Matrix.stdBasisMatrix i j x) = x ⊗ₜ[R] Matrix.stdBasisMatrix i j 1

Alias of matrixEquivTensor_apply_stdBasisMatrix.

@[simp]

theorem matrixEquivTensor_apply_symm (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (a : A) (M : Matrix n n R) : (matrixEquivTensor n R A).symm (a ⊗ₜ[R] M) = M.map fun (x : R) => a * (algebraMap R A) x