TensorCoefficientMatrix.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The trace-pairing bridge from invariant multilinear forms to the commutant of finite tensor powers.

theorem OAI.KadisonSimilarity.tensorMatrixUnit_as_single line 17
theorem OAI.KadisonSimilarity.matrix_eq_sum_tensorMatrixUnit line 22

theorem OAI.KadisonSimilarity.multilinear_matrix_expansion line 28

Source documentation

Expansion in matrix units, keeping one row and column label per slot.

theorem multilinear_matrix_expansion
    (F : MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ)
    (v : ι → Matrix α α ℂ) :
    F v = ∑ r : ι → α, ∑ c : ι → α,
      (∏ i, v i (r i) (c i)) * F (fun i => tensorMatrixUnit (r i) (c i)) := by
…

Mentions: OAI.KadisonSimilarity.tensorMatrixUnit

def OAI.KadisonSimilarity.tensorCoefficientMatrix line 47
Source documentation
The transposed matrix-unit coefficients give the trace-dual matrix.
```
def tensorCoefficientMatrix
    (F : MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ) :
    Matrix (ι → α) (ι → α) ℂ :=
…
```
theorem OAI.KadisonSimilarity.multilinear_eq_trace_tensorCoefficient line 52
theorem OAI.KadisonSimilarity.tupleTensorMatrix_matrixUnits line 67

theorem OAI.KadisonSimilarity.eq_of_trace_tupleTensorMatrix_eq line 78

Source documentation

Tensor products of matrix units separate the trace pairing.

theorem eq_of_trace_tupleTensorMatrix_eq (A B : Matrix (ι → α) (ι → α) ℂ)
    (h : ∀ v : ι → Matrix α α ℂ,
      Matrix.trace (A * tupleTensorMatrix v) = Matrix.trace (B * tupleTensorMatrix v)) : A = B := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix

theorem OAI.KadisonSimilarity.tensorCoefficientMatrix_commutes_unitary line 88

Source documentation

An invariant form has a trace-dual matrix commuting with every tensor power of a unitary.

theorem tensorCoefficientMatrix_commutes_unitary
    (F : MultilinearMap ℂ (fun _ : ι => Matrix α α ℂ) ℂ)
    (hF : UnitaryConjugationInvariant F) (u : Matrix.unitaryGroup α ℂ) :
    tensorCoefficientMatrix F * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
      tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * tensorCoefficientMatrix F := by
…

Mentions: OAI.KadisonSimilarity.UnitaryConjugationInvariant, OAI.KadisonSimilarity.tensorCoefficientMatrix, OAI.KadisonSimilarity.tupleTensorMatrix