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

noncomputable def MatrixEquivTensor.toFunBilinear (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [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

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

@[simp]

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

noncomputable def MatrixEquivTensor.toFunLinear (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [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

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

noncomputable def MatrixEquivTensor.toFunAlgHom (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [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 R A n = Algebra.TensorProduct.algHomOfLinearMapTensorProduct (MatrixEquivTensor.toFunLinear R A n) ⋯ ⋯

@[simp]

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

noncomputable def MatrixEquivTensor.invFun (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [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 R A n M = Finset.sum Finset.univ fun (p : n × n) => M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1

@[simp]

theorem MatrixEquivTensor.invFun_zero (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] : MatrixEquivTensor.invFun R A n 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

theorem MatrixEquivTensor.right_inv (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (M : Matrix n n A) : (MatrixEquivTensor.toFunAlgHom R A n) (MatrixEquivTensor.invFun R A n M) = M

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

noncomputable def MatrixEquivTensor.equiv (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [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 R A n = { toFun := ⇑(MatrixEquivTensor.toFunAlgHom R A n), invFun := MatrixEquivTensor.invFun R A n, left_inv := ⋯, right_inv := ⋯ }

noncomputable def matrixEquivTensor (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [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 (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (M : Matrix n n A) : (matrixEquivTensor R A n) M = Finset.sum Finset.univ 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) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (i : n) (j : n) (x : A) : (matrixEquivTensor R A n) (Matrix.stdBasisMatrix i j x) = x ⊗ₜ[R] Matrix.stdBasisMatrix i j 1

@[simp]

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