Tensor products of matrix algebras

This file records the finite-index form of the Kronecker equivalence for tensor products of matrix algebras.

Main result

• Matrix.finOneAlgEquiv: the canonical equivalence A ≃ₐ[R] M₁(A) using Fin 1 indices.
• Matrix.kroneckerTMulFinAlgEquiv: matrix absorption M_m(A) ⊗[R] M_n(B) ≃ₐ[R] M_(mn)(A ⊗[R] B).
• Matrix.kroneckerFinAlgEquiv: its scalar case M_m(R) ⊗[R] M_n(R) ≃ₐ[R] M_(mn)(R).

def Matrix.finOneAlgEquiv (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : A ≃ₐ[R] Matrix (Fin 1) (Fin 1) A

The canonical one-by-one matrix equivalence with Fin 1 indices.

Equations

• Matrix.finOneAlgEquiv R A = Matrix.uniqueAlgEquiv.symm.trans (Matrix.reindexAlgEquiv R A (Equiv.ofUnique Unit (Fin 1)))

@[simp]

theorem Matrix.finOneAlgEquiv_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (i j : Fin 1) : (finOneAlgEquiv R A) a i j = a

The one-by-one matrix equivalence sends a scalar to the constant one-by-one matrix.

@[simp]

theorem Matrix.finOneAlgEquiv_symm_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (M : Matrix (Fin 1) (Fin 1) A) : (finOneAlgEquiv R A).symm M = M 0 0

The inverse one-by-one matrix equivalence extracts the unique entry.

def Matrix.kroneckerTMulFinAlgEquiv (m n : ℕ) (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] : TensorProduct R (Matrix (Fin m) (Fin m) A) (Matrix (Fin n) (Fin n) B) ≃ₐ[R] Matrix (Fin (m * n)) (Fin (m * n)) (TensorProduct R A B)

Matrix absorption: M_m(A) ⊗[R] M_n(B) ≃ₐ[R] M_(mn)(A ⊗[R] B), over any commutative semiring R and any two R-algebras, in any two sizes.

Equations

• Matrix.kroneckerTMulFinAlgEquiv m n R A B = (Matrix.kroneckerTMulAlgEquiv (Fin m) (Fin n) R R A B).trans (Matrix.reindexAlgEquiv R (TensorProduct R A B) finProdFinEquiv)

@[simp]

theorem Matrix.kroneckerTMulFinAlgEquiv_tmul (m n : ℕ) (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (a : Matrix (Fin m) (Fin m) A) (b : Matrix (Fin n) (Fin n) B) : (kroneckerTMulFinAlgEquiv m n R A B) (a ⊗ₜ[R] b) = (reindex finProdFinEquiv finProdFinEquiv) (kroneckerMap (TensorProduct.tmul R) a b)

The finite-index matrix absorption equivalence sends a pure tensor to the reindexed Kronecker tensor product.

@[simp]

theorem Matrix.kroneckerTMulFinAlgEquiv_symm_single_tmul (m n : ℕ) (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (B : Type u_3) [Semiring B] [Algebra R B] (ia ja : Fin m) (ib jb : Fin n) (a : A) (b : B) : (kroneckerTMulFinAlgEquiv m n R A B).symm (single (finProdFinEquiv (ia, ib)) (finProdFinEquiv (ja, jb)) (a ⊗ₜ[R] b)) = single ia ja a ⊗ₜ[R] single ib jb b

The inverse finite-index matrix absorption equivalence sends a matrix unit at paired finite indices with a pure-tensor coefficient to the tensor of the two corresponding matrix units.

def Matrix.kroneckerFinAlgEquiv (m n : ℕ) (R : Type u_1) [CommSemiring R] : TensorProduct R (Matrix (Fin m) (Fin m) R) (Matrix (Fin n) (Fin n) R) ≃ₐ[R] Matrix (Fin (m * n)) (Fin (m * n)) R

The Kronecker product identifies M_m(R) ⊗[R] M_n(R) with M_(mn)(R), with Fin indices.

Equations

• Matrix.kroneckerFinAlgEquiv m n R = (Matrix.kroneckerAlgEquiv (Fin m) (Fin n) R).trans (Matrix.reindexAlgEquiv R R finProdFinEquiv)

@[simp]

theorem Matrix.kroneckerFinAlgEquiv_tmul (m n : ℕ) (R : Type u_1) [CommSemiring R] (a : Matrix (Fin m) (Fin m) R) (b : Matrix (Fin n) (Fin n) R) : (kroneckerFinAlgEquiv m n R) (a ⊗ₜ[R] b) = (reindex finProdFinEquiv finProdFinEquiv) (kroneckerMap (fun (x1 x2 : R) => x1 * x2) a b)

The finite-index Kronecker equivalence sends a pure tensor to the reindexed Kronecker product.