TensorCommutantExtension.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Extending a tensor commutation identity from unitary matrices to all matrices. Diagonal weights, Hermitian diagonalization and a polynomial identity suffice; no decomposition of a general matrix is assumed.

theorem OAI.KadisonSimilarity.tensor_commutant_commutes_hermitian line 21

Source documentation

Commutation with unitary tensor powers implies commutation with every Hermitian tensor power.

theorem tensor_commutant_commutes_hermitian
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ u : Matrix.unitaryGroup α ℂ,
      C * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
        tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * C)
    (a : Matrix α α ℂ) (ha : a.IsHermitian) :
    C * tupleTensorMatrix (fun _ : ι => a) =
      tupleTensorMatrix (fun _ : ι => a) * C := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix

def OAI.KadisonSimilarity.tensorCommutatorPolynomial line 57
theorem OAI.KadisonSimilarity.tensorCommutatorPolynomial_eval line 65

theorem OAI.KadisonSimilarity.tensor_commutes_complex_line line 78

Source documentation

A polynomial commutation identity on a real line also holds on its complexification.

theorem tensor_commutes_complex_line
    (C : Matrix (ι → α) (ι → α) ℂ) (a b : Matrix α α ℂ)
    (h : ∀ t : ℝ,
      C * tupleTensorMatrix (fun _ : ι => a + (t : ℂ) • b) =
        tupleTensorMatrix (fun _ : ι => a + (t : ℂ) • b) * C)
    (z : ℂ) :
    C * tupleTensorMatrix (fun _ : ι => a + z • b) =
      tupleTensorMatrix (fun _ : ι => a + z • b) * C := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix

theorem OAI.KadisonSimilarity.tensor_commutant_commutes_matrix line 98

Source documentation

The exact unitary-to-all-matrices extension needed for finite tensor Schur--Weyl spanning.

theorem tensor_commutant_commutes_matrix
    (C : Matrix (ι → α) (ι → α) ℂ)
    (hC : ∀ u : Matrix.unitaryGroup α ℂ,
      C * tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) =
        tupleTensorMatrix (fun _ : ι => (u : Matrix α α ℂ)) * C)
    (a : Matrix α α ℂ) :
    C * tupleTensorMatrix (fun _ : ι => a) =
      tupleTensorMatrix (fun _ : ι => a) * C := by
…

Mentions: OAI.KadisonSimilarity.tupleTensorMatrix