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 : Basis ι R M)
(bN : Basis κ R N)
(bM' : Basis ι' R M')
(bN' : Basis κ' R N')
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
:
(LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.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 : Basis ι R M)
(bN : Basis κ R N)
(bM' : Basis ι' R M')
(bN' : Basis κ' R N')
(A : Matrix ι' ι R)
(B : Matrix κ' κ R)
:
(Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B) = TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.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 : Basis ι R M)
(bN : 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 : Basis ι R M)
(bN : Basis κ R N)
(bP : 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.