TensorContract of inverse matrix

Question

Matrix inverse in mathematica

If $A$ is an invertible $n \times n$ matrix, then $A\cdot A^{-1} = I$.

To get this statement in Mathematica, you need the assumption
MatrixPower[A, 0] = IdentityMatrix[n]

$Assumptions = {Element[A, Matrices[{n, n}]], 
                Det[A] != 0, ForAll[{A}, MatrixPower[A, 0] == IdentityMatrix[n]]}
TensorExpand[Inverse[A].A] // Simplify

Out[1]= IdentityMatrix[n].

Matrix as a tensor

A matrix can also be seen as a tensor of rank 2; i.e. a list with two levels, on for the columns and one for the rows. The tensor product $A \otimes A^{-1}$ corresponds in Mathematica with the outer product of the two lists. In this case it is a list with four levels, a four-tensor.

When matrices are viewed as tensors, the dot product is the same as a tensor product followed by a contraction. In Mathematica the matrix product $A\cdot A^{-1}$ can also be written as

TensorContract[Inverse[A]\[TensorProduct]A, {2, 3}] 

Question 1

How can I let Mathematica evaluate the above expression to IdentityMatrix[n]?

Involving more tensors

Suppose there is a second $n \times n$ matrix $B$. In that case one can think of more complex tensor products, for example $B \otimes A \otimes A^{-a}$. This is a rank 6 tensor.

Contracting slots 3 and 4 of the 6-tensor gives 4-tensor $B \otimes I$, where $I$ is the identity matrix. In Mathematica, this contraction can be written as

TensorContract[B\[TensorProduct]A\[TensorProduct]Inverse[A], {3, 4}] 

Question 2
Also for the above contraction, I would like Mathematica to use the idenity $A\cdot A^{-1} = I$. It should evaluate to

B\[TensorProduct]A\[TensorProduct]Inverse[A], {3, 4}] 

More over, I want Mathematica to use the same identity in more complicated tensor products, like $ B \otimes A \otimes B \otimes A^{-1} $. The last example should evaluate to

TensorTranspose[B \otimes I \otimes B, {{4, 5}]

How can this be realized with Mathematica 9?

Generalizations

Ihe above, there was allays only one invertible matrix which was called $A$.
Question 3
Can you take identity relations are into account for any invertible matrix, irrespectively of the names or number of invertible matrices?

Answer 1

Here's a rule that I think captures the spirit of what you're trying to do. (EDIT: Needed to shuffle some of the indices around to get the identity matrix into the right spot. SECOND EDIT: Treat the case of both left and right contraction.)

$Assumptions = 
 A ∈ Matrices[{n, n}] && 
  Inverse[A] ∈ Matrices[{n, n}] && Det[A] != 0 && 
  ForAll[{A}, MatrixPower[A, 0] == IdentityMatrix[n]] && 
  a ∈ Matrices[{n, n}] && b ∈ Matrices[{n, n}] && 
  c ∈ Matrices[{n, n}];

contractinv = 
 Quiet[{TensorContract[
     a___\[TensorProduct]A_\[TensorProduct]b___\[TensorProduct]B_\
\[TensorProduct]c___, {i1___, {m_, n_}, 
      i2___}] :> (TensorContract[
       TensorTranspose[
        a\[TensorProduct]IdentityMatrix[
          First[TensorDimensions[
            A]]]\[TensorProduct]b\[TensorProduct]c, 
        Join[Range[Min[m, n] - 1], {Max[m, n] - 1}, 
         Range[Min[m, n], Max[m, n] - 2]]], {i1, 
         i2} /. {i_ /; i > Max[m, n] :> i - 2}]) /; (B == Inverse[A] ||
         A == Inverse[B]) && m == 2 Length[{a}] + 2 && 
      n == 2 Length[{a, b}] + 3, 
   TensorContract[
     a___\[TensorProduct]A_\[TensorProduct]b___\[TensorProduct]B_\
\[TensorProduct]c___, {i1___, {m_, n_}, 
      i2___}] :> (TensorContract[
       TensorTranspose[
        a\[TensorProduct]IdentityMatrix[
          First[TensorDimensions[
            A]]]\[TensorProduct]b\[TensorProduct]c, 
        Join[Range[Min[m, n]], {Max[m, n] - 2}, 
         Range[Min[m, n] + 1, Max[m, n] - 3]]], {i1, 
         i2} /. {i_ /; i > Max[m, n] :> i - 2}]) /; (B == Inverse[A] ||
         A == Inverse[B]) && m == 2 Length[{a}] + 1 && 
      n == 2 Length[{a, b}] + 4}]

Which gives for a simple test:

TensorContract[
  a\[TensorProduct]Inverse[
    A]\[TensorProduct]b\[TensorProduct]A\[TensorProduct]c, {{2, 
    3}, {4, 7}, {8, 9}}] /. contractinv
(* TensorContract[a\[TensorProduct]b\[TensorProduct]c, {{2, 3}, {4, 7}}] *)

TensorContract[Inverse[A]\[TensorProduct]A,{{2,3}}]/.contractinv
(* IdentityMatrix[n] *)