mathlib3 documentation

linear_algebra.tensor_product.matrix

Connections between tensor_product and matrix #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains results about the matrices corresponding to maps between tensor product types, where the correspondance is induced by basis.tensor_product

Notably, tensor_product.to_matrix_map shows that taking the tensor product of linear maps is equivalent to taking the kronecker product of their matrix representations.

source
theorem tensor_product.to_matrix_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} [decidable_eq ι] [decidable_eq κ] [fintype ι] [fintype κ] [fintype ι'] [fintype κ'] [comm_ring R] [add_comm_group M] [add_comm_group N] [add_comm_group M'] [add_comm_group N'] [module R M] [module R N] [module R M'] [module R N'] (bM : basis ι R M) (bN : basis κ R N) (bM' : basis ι' R M') (bN' : basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N') :
⇑(linear_map.to_matrix (bM.tensor_product bN) (bM'.tensor_product bN')) (tensor_product.map f g) = matrix.kronecker_map has_mul.mul (⇑(linear_map.to_matrix bM bM') f) (⇑(linear_map.to_matrix bN bN') g)

The linear map built from tensor_product.map corresponds to the matrix built from matrix.kronecker.

source
theorem matrix.to_lin_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} [decidable_eq ι] [decidable_eq κ] [fintype ι] [fintype κ] [fintype ι'] [fintype κ'] [comm_ring R] [add_comm_group M] [add_comm_group N] [add_comm_group M'] [add_comm_group N'] [module R M] [module R N] [module R M'] [module R N'] (bM : basis ι R M) (bN : basis κ R N) (bM' : basis ι' R M') (bN' : basis κ' R N') (A : matrix ι' ι R) (B : matrix κ' κ R) :
⇑(matrix.to_lin (bM.tensor_product bN) (bM'.tensor_product bN')) (matrix.kronecker_map has_mul.mul A B) = tensor_product.map (⇑(matrix.to_lin bM bM') A) (⇑(matrix.to_lin bN bN') B)

The matrix built from matrix.kronecker corresponds to the linear map built from tensor_product.map.

source
theorem tensor_product.to_matrix_comm {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [decidable_eq ι] [decidable_eq κ] [fintype ι] [fintype κ] [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] (bM : basis ι R M) (bN : basis κ R N) :
⇑(linear_map.to_matrix (bM.tensor_product bN) (bN.tensor_product bM)) ↑(tensor_product.comm R M N) = 1.submatrix prod.swap id

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

source
theorem tensor_product.to_matrix_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} [decidable_eq ι] [decidable_eq κ] [decidable_eq τ] [fintype ι] [fintype κ] [fintype τ] [comm_ring R] [add_comm_group M] [add_comm_group N] [add_comm_group P] [module R M] [module R N] [module R P] (bM : basis ι R M) (bN : basis κ R N) (bP : basis τ R P) :
⇑(linear_map.to_matrix ((bM.tensor_product bN).tensor_product bP) (bM.tensor_product (bN.tensor_product bP))) ↑(tensor_product.assoc R M N P) = 1.submatrix id ⇑(equiv.prod_assoc ι κ τ)

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