TensorStableSpanning.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Schur--Weyl spanning in the stable range needed after taking a cofinal tail of the matrix tower. The proof uses a single column with distinct labels.

theorem OAI.KadisonSimilarity.exists_permutation_of_tensor_weights line 17
def OAI.KadisonSimilarity.tensorColumnTransfer line 38
theorem OAI.KadisonSimilarity.tensorColumnTransfer_apply line 42
theorem OAI.KadisonSimilarity.tensorColumnTransfer_column line 49

theorem OAI.KadisonSimilarity.tensor_commutant_eq_zero_of_column line 60

Source documentation

A matrix commuting with every tensor power is determined by its column at any elementary tensor whose labels are distinct.

theorem tensor_commutant_eq_zero_of_column
    (j : ι → α) (hj : Function.Injective j)
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ a : Matrix α α ℂ,
      C * tupleTensorMatrix (fun _ : ι => a) =
        tupleTensorMatrix (fun _ : ι => a) * C)
    (hcolumn : ∀ f, C f j = 0) : C = 0 := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix

theorem OAI.KadisonSimilarity.tensor_commutant_spanned_by_permutations line 76

Source documentation

The full tensor commutant is spanned by coordinate permutations once a tuple of distinct labels is available.

theorem tensor_commutant_spanned_by_permutations
    (j : ι → α) (hj : Function.Injective j)
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ u : Matrix.unitaryGroup α ℂ,
      C * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
        tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * C) :
    ∃ c : Equiv.Perm ι → ℂ, C = ∑ π, c π • tensorPermutationMatrix (α := α) π := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix, OAI.KadisonSimilarity.tensorPermutationMatrix

theorem OAI.KadisonSimilarity.schurWeylMultilinearSpanning_of_labels line 130
Source documentation
The stable-range specialization of the published Schur--Weyl input.
```
theorem schurWeylMultilinearSpanning_of_labels [Nonempty α]
    (j : ι → α) (hj : Function.Injective j) : SchurWeylMultilinearSpanning ι α := by
…
```
Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning