TensorPermutations.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Permutations of completed Hilbert tensor words

The permutation maps are constructed from the multilinear universal property and proved isometric on the algebraic tensor power before completion.

theorem OAI.KadisonSimilarity.tensorWord_update_add line 21
theorem OAI.KadisonSimilarity.tensorWord_update_smul line 43
def OAI.KadisonSimilarity.tensorWordMultilinear line 64
Source documentation
The elementary word map, with its multilinearity bundled.
```
def tensorWordMultilinear (n : ℕ) : MultilinearMap ℂ (fun _ : Fin n => E) (TensorWord E n) :=
…
```
Mentions: OAI.KadisonSimilarity.TensorWord
theorem OAI.KadisonSimilarity.tensorWordMultilinear_apply line 67

def OAI.KadisonSimilarity.tensorWordLiftLinear line 73

Source documentation

The multilinear universal property of the iterated algebraic tensor word.

def tensorWordLiftLinear (F : Type*) [AddCommGroup F] [Module ℂ F] :
    (n : ℕ) → MultilinearMap ℂ (fun _ : Fin n => E) F →ₗ[ℂ] (TensorWord E n →ₗ[ℂ] F)
  | 0 =>
    { toFun := fun f =>
…

Mentions: OAI.KadisonSimilarity.TensorWord

theorem OAI.KadisonSimilarity.tensorWordLiftLinear_apply_word line 103
theorem OAI.KadisonSimilarity.linearMap_ext_tensorWords line 119
Source documentation
Algebraic linear maps on tensor words are determined by elementary words.
```
theorem linearMap_ext_tensorWords {F : Type*} [AddCommGroup F] [Module ℂ F] {n : ℕ}
    (f g : TensorWord E n →ₗ[ℂ] F)
    (hword : ∀ x : Fin n → E, f (tensorWord x) = g (tensorWord x)) : f = g := by
…
```
Mentions: OAI.KadisonSimilarity.TensorWord, OAI.KadisonSimilarity.tensorWord
def OAI.KadisonSimilarity.tensorPermutationLinear line 129
Source documentation
The algebraic map permuting tensor positions.
```
def tensorPermutationLinear {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    TensorWord E n →ₗ[ℂ] TensorWord E n :=
…
```
Mentions: OAI.KadisonSimilarity.TensorWord
theorem OAI.KadisonSimilarity.tensorPermutationLinear_word line 133
theorem OAI.KadisonSimilarity.linearMap_preserves_inner_of_words line 139
def OAI.KadisonSimilarity.tensorPermutationIsometry line 159
Source documentation
Tensor-position permutations preserve the Hilbert inner product.
```
def tensorPermutationIsometry {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    TensorWord E n →ₗᵢ[ℂ] TensorWord E n :=
…
```
Mentions: OAI.KadisonSimilarity.TensorWord
def OAI.KadisonSimilarity.completedTensorPermutation line 167
Source documentation
The corresponding permutation on the completed Hilbert tensor power.
```
def completedTensorPermutation {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    CompletedTensorWord E n →ₗᵢ[ℂ] CompletedTensorWord E n :=
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord
theorem OAI.KadisonSimilarity.completedTensorPermutation_word line 171
theorem OAI.KadisonSimilarity.completedTensorPermutation_inverse line 182
theorem OAI.KadisonSimilarity.completedTensorPermutation_constant line 193
Source documentation
Every tensor-position permutation fixes a repeated-letter tensor.
```
@[simp] theorem completedTensorPermutation_constant {n : ℕ}
    (σ : Equiv.Perm (Fin n)) (x : E) :
    completedTensorPermutation σ (completedTensorWord (fun _ : Fin n => x)) =
      completedTensorWord (fun _ : Fin n => x) := by
…
```
Mentions: OAI.KadisonSimilarity.completedTensorPermutation, OAI.KadisonSimilarity.completedTensorWord