Connections between TensorProduct and Matrix

This file contains results about the matrices corresponding to maps between tensor product types, where the correspondence is induced by Basis.tensorProduct

Notably, TensorProduct.toMatrix_map shows that taking the tensor product of linear maps is equivalent to taking the Kronecker product of their matrix representations.

theorem TensorProduct.toMatrix_map {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N') : (LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (map f g) = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g)

The linear map built from TensorProduct.map corresponds to the matrix built from Matrix.kronecker.

theorem Matrix.toLin_kronecker {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (A : Matrix ι' ι R) (B : Matrix κ' κ R) : (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B) = TensorProduct.map ((toLin bM bM') A) ((toLin bN bN') B)

The matrix built from Matrix.kronecker corresponds to the linear map built from TensorProduct.map.

theorem TensorProduct.toMatrix_comm {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) : (LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = Matrix.submatrix 1 Prod.swap id

TensorProduct.comm corresponds to a permutation of the identity matrix.

theorem TensorProduct.toMatrix_assoc {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {ι : Type u_7} {κ : Type u_8} {τ : Type u_9} [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [Fintype ι] [Fintype κ] [Fintype τ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bP : Module.Basis τ R P) : (LinearMap.toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))) ↑(TensorProduct.assoc R M N P) = Matrix.submatrix 1 id ⇑(Equiv.prodAssoc ι κ τ)

TensorProduct.assoc corresponds to a permutation of the identity matrix.