TensorMatrixAlgebra.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Finite tensor matrices and the invariance of permutation contractions. These coordinate calculations supply the spanning generators for the local Schur--Weyl argument.

def OAI.KadisonSimilarity.tupleTensorMatrix line 18
Source documentation
The matrix of a tensor product of finitely many matrix operators.
```
def tupleTensorMatrix (v : ι → Matrix α α ℂ) : Matrix (ι → α) (ι → α) ℂ :=
…
```
theorem OAI.KadisonSimilarity.tupleTensorMatrix_apply line 22
theorem OAI.KadisonSimilarity.tupleTensorMatrix_mul line 26
theorem OAI.KadisonSimilarity.tupleTensorMatrix_one line 33
theorem OAI.KadisonSimilarity.tupleTensorMatrix_star line 41
def OAI.KadisonSimilarity.tensorCoordinatePermutation line 47
Source documentation
Reordering the tensor coordinates.
```
def tensorCoordinatePermutation (π : Equiv.Perm ι) : Equiv.Perm (ι → α) where
…
```
def OAI.KadisonSimilarity.tensorPermutationMatrix line 54
Source documentation
Its matrix uses the same successor convention as permutationContraction.
```
def tensorPermutationMatrix (π : Equiv.Perm ι) : Matrix (ι → α) (ι → α) ℂ :=
…
```
theorem OAI.KadisonSimilarity.tensorMatrix_mul_permutation line 57
theorem OAI.KadisonSimilarity.permutation_mul_tensorMatrix line 63
theorem OAI.KadisonSimilarity.constant_tensorMatrix_commutes_permutation line 69
theorem OAI.KadisonSimilarity.permutationContraction_eq_trace line 78

theorem OAI.KadisonSimilarity.permutationContraction_unitary_conjugate line 86

Source documentation

Simultaneous unitary conjugation preserves every permutation contraction.

theorem permutationContraction_unitary_conjugate (π : Equiv.Perm ι)
    (u : Matrix.unitaryGroup α ℂ) (v : ι → Matrix α α ℂ) :
    permutationContraction π (fun i =>
      (u : Matrix α α ℂ) * v i * star (u : Matrix α α ℂ)) =
        permutationContraction π v := by
…

Mentions: OAI.KadisonSimilarity.permutationContraction

theorem OAI.KadisonSimilarity.permutationContractionMultilinear_invariant line 105
theorem OAI.KadisonSimilarity.normalizedPermutationMultilinear_invariant line 111