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.

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') :

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

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) :

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

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) :

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

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) :

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