Mixed product identity between tensors in Mathematica 9

Question

How can we simplify tensor expressions in Mathematica 9 using the mixed-product identity $(A\otimes B)(C \otimes D) \equiv AC \otimes BD$ ?

Is it possible to implement this kind of evaluations using the new Mathematica 9 tensor capabilities?

The following expression is false:

TensorProduct[a, b].TensorProduct[c, d] === TensorProduct[ a.c, b.d]

I don't really need to prove this identity, but rather to use it for simplifying some expressions. In my case, $a$ and $c$ are some (unknown) symbolic matrices, while $b$ and $d$ are explicit integer $2\times 2$ matrices. I'd like Mathematica to evaluate the matrix product between $b$ and $d$ explicitly.

For instance, when

b=PauliMatrix[1]; d=PauliMatrix[3];

as the product of two Pauli matrices gives another Pauli matrix, I'd like to obtain the simplified result

TensorProduct[a.c, -I PauliMatrix[2]]

Answer 1

You could also do

$Assumptions = (a | b | c | d) \[Element] Matrices[{k, k}]

KroneckerProduct[a, b] . KroneckerProduct[c, d] // TensorExpand

which returns

KroneckerProduct[a.c, b.d]

Answer 2

1. The mixed-product identity

   $$ (A\otimes B)(C \otimes D) \equiv AC \otimes BD$$

   is written in terms of the Kronecker product (see here) not TensorProduct. They have different dimensions

   A = RandomReal[1.0, {10, 10}];
   KroneckerProduct[A, A] // Dimensions
   TensorProduct[A, A] // Dimensions
   

   {100, 100}
   {10, 10, 10, 10}
   

2. lhs === rhs gives exact comparison of lhs and rhs. You need to use ==.

3. Unfortunately tensors operations with KroneckerProduct and Dot is not fully implemented in Mathematica 9. However, for example, Dot[a,b] is equivalent to TensorContract[a\[TensorProduct]b, {{2, 3}}].

Finally, you can rewrite your identity as

$Assumptions = (a | b | c | d) \[Element] Matrices[{k, k}];

TensorTranspose[
   TensorContract[a\[TensorProduct]b\[TensorProduct]c\[TensorProduct]d, {{2, 5}, {4, 7}}], 
 {1, 3, 2, 4}] == 
 TensorContract[a\[TensorProduct]c, {{2, 3}}]\[TensorProduct]TensorContract[
   b\[TensorProduct]d, {{2, 3}}] // TensorReduce

True

Unfortunately, I can't explain derivation of this formula because I don't understand it completely.