Algebra isomorphisms between tensor products and matrices

Main definitions

• matrixEquivTensor : Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).
• Matrix.kroneckerTMulAlgEquiv : Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B), where the forward map is the (tensor-ified) Kronecker product.

def kroneckerTMulLinearEquiv (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] : TensorProduct R (Matrix l m M) (Matrix n p N) ≃ₗ[S] Matrix (l × n) (m × p) (TensorProduct R M N)

Matrix.kroneckerTMul as a linear equivalence, when the two arguments are tensored.

@[simp]

theorem kroneckerTMulLinearEquiv_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (a : Matrix l m M) (b : Matrix n p N) : (kroneckerTMulLinearEquiv l m n p R S M N) (a ⊗ₜ[R] b) = Matrix.kroneckerMap (fun (x1 : M) (x2 : N) => x1 ⊗ₜ[R] x2) a b

@[simp]

theorem kroneckerTMulAlgEquiv_symm_single_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b

@[deprecated kroneckerTMulAlgEquiv_symm_single_tmul (since := "2025-05-05")]

theorem kroneckerTMulAlgEquiv_symm_stdBasisMatrix_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b

Alias of kroneckerTMulAlgEquiv_symm_single_tmul.

@[simp]

theorem kroneckerTMulLinearEquiv_one (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] : (kroneckerTMulLinearEquiv m m n n R S A B) 1 = 1

@[simp]

theorem kroneckerTMulLinearEquiv_mul (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] (x y : TensorProduct R (Matrix m m A) (Matrix n n B)) : (kroneckerTMulLinearEquiv m m n n R S A B) (x * y) = (kroneckerTMulLinearEquiv m m n n R S A B) x * (kroneckerTMulLinearEquiv m m n n R S A B) y

Note this can't be stated for rectangular matrices because there is no HMul (TensorProduct R _ _) (TensorProduct R _ _) (TensorProduct R _ _) instance.

def MatrixEquivTensor.toFunBilinear (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.

@[simp]

theorem MatrixEquivTensor.toFunBilinear_apply (n : Type u_3) (R : Type u_5) (A : Type u_7) [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)

def MatrixEquivTensor.toFunLinear (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.

def MatrixEquivTensor.toFunAlgHom (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.

@[simp]

theorem MatrixEquivTensor.toFunAlgHom_apply (n : Type u_3) (R : Type u_5) (A : Type u_7) [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)

def MatrixEquivTensor.invFun (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.)

@[simp]

theorem MatrixEquivTensor.invFun_zero (n : Type u_3) (R : Type u_5) (A : Type u_7) [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_3) (R : Type u_5) (A : Type u_7) [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_3) (R : Type u_5) (A : Type u_7) [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_3) (R : Type u_5) (A : Type u_7) [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_3) (R : Type u_5) (A : Type u_7) [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_3) (R : Type u_5) (A : Type u_7) [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

def MatrixEquivTensor.equiv (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.

def matrixEquivTensor (n : Type u_3) (R : Type u_5) (A : Type u_7) [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).

@[simp]

theorem matrixEquivTensor_apply (n : Type u_3) (R : Type u_5) (A : Type u_7) [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.single p.1 p.2 1

@[simp]

theorem matrixEquivTensor_apply_single (n : Type u_3) (R : Type u_5) (A : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (i j : n) (x : A) : (matrixEquivTensor n R A) (Matrix.single i j x) = x ⊗ₜ[R] Matrix.single i j 1

@[deprecated matrixEquivTensor_apply_single (since := "2025-05-05")]

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

Alias of matrixEquivTensor_apply_single.

@[simp]

theorem matrixEquivTensor_apply_symm (n : Type u_3) (R : Type u_5) (A : Type u_7) [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) = a • M.map ⇑(algebraMap R A)

def Matrix.kroneckerTMulAlgEquiv (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) (B : Type u_8) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] : TensorProduct R (Matrix m m A) (Matrix n n B) ≃ₐ[S] Matrix (m × n) (m × n) (TensorProduct R A B)

Matrix.kroneckerTMul as an algebra equivalence, when the two arguments are tensored.

@[simp]

theorem Matrix.kroneckerTMulAlgEquiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : TensorProduct R (Matrix m m A) (Matrix n n B)) : (kroneckerTMulAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x

@[simp]

theorem Matrix.kroneckerTMulAlgEquiv_symm_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : Matrix (m × n) (m × n) (TensorProduct R A B)) : (kroneckerTMulAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x