MatrixBlockSwap.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite permutations and block swaps of matrix units

These unitaries are finite sums of the given matrix units. No trace, infinite tensor product, or existence premise is involved.

def OAI.KadisonKastler.matrixPermutationValue line 24
Source documentation
The permutation matrix in an actual system of matrix units.
```
def matrixPermutationValue (E : MatrixUnitSystem ι A) (e : Equiv.Perm ι) : A :=
…
```
theorem OAI.KadisonKastler.matrixPermutationValue_mul_entry line 27
theorem OAI.KadisonKastler.matrixPermutationValue_mul line 37
theorem OAI.KadisonKastler.matrixPermutationValue_one line 46
theorem OAI.KadisonKastler.matrixPermutationValue_star line 49
def OAI.KadisonKastler.matrixPermutationUnitary line 58
Source documentation
The finite permutation sum is an actual unitary.
```
def matrixPermutationUnitary (E : MatrixUnitSystem ι A) (e : Equiv.Perm ι) : unitary A :=
…
```
theorem OAI.KadisonKastler.matrixPermutationUnitary_conjugate_entry line 64
def OAI.KadisonKastler.finiteMatrixBlockSwap line 79
Source documentation
The unitary exchanging two equal finite tensor blocks.
```
def finiteMatrixBlockSwap (E : MatrixUnitSystem (ι × ι) A) : unitary A :=
…
```
theorem OAI.KadisonKastler.finiteMatrixBlockSwap_value line 82

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_conjugate_entry line 89

Source documentation

Block swapping exchanges the two indices on each side.

theorem finiteMatrixBlockSwap_conjugate_entry (E : MatrixUnitSystem (ι × ι) A)
    (i j k l : ι) :
    (finiteMatrixBlockSwap E : A) * E.entry (i, j) (k, l) * star (finiteMatrixBlockSwap E : A) =
      E.entry (j, i) (l, k) :=
…

Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap

theorem OAI.KadisonKastler.finiteMatrixBlockSwap_mem line 96
Source documentation
The swap belongs to the same finite matrix algebra.
```
theorem finiteMatrixBlockSwap_mem [StarModule ℂ A] (E : MatrixUnitSystem (ι × ι) A) :
    (finiteMatrixBlockSwap E : A) ∈ E.algebra := by
…
```
Mentions: OAI.KadisonKastler.finiteMatrixBlockSwap