OAI/Analysis/KadisonSimilarity/Tracial/TracialStageCommutation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Commutation with all matrix stages extends to the represented source by density of trace vectors in the actual normal ambient algebra.

  1. def OAI.KadisonSimilarity.relativeOperatorCommutant line 18
  2. theorem OAI.KadisonSimilarity.relativeOperatorCommutant_le line 27
  3. theorem OAI.KadisonSimilarity.relativeOperatorCommutant_mem line 37
  4. theorem OAI.KadisonSimilarity.relativeOperatorCommutant_commutes line 50
  5. theorem OAI.KadisonSimilarity.commutes_source_of_matrix_stages line 70

    Source documentation

    The original GNS action commutes with every operator commuting with the stages.

    theorem commutes_source_of_matrix_stages (Z : τB.GNS →L[ℂ] τB.GNS)
    (hZ : ∀ j a, Z * τB.gnsStarAlgHom (ρ (M.embedding j a)) =
      τB.gnsStarAlgHom (ρ (M.embedding j a)) * Z) (r : R) :
    Z * τB.gnsStarAlgHom (ρ r) = τB.gnsStarAlgHom (ρ r) * Z := by
…
  6. theorem OAI.KadisonSimilarity.commutes_amplified_source_of_matrix_stages line 109

    Source documentation

    Coordinate compression extends stage commutation at every finite multiplicity.

    theorem commutes_amplified_source_of_matrix_stages (n : ℕ)
    (Y : HilbertCopies τB.GNS n →L[ℂ] HilbertCopies τB.GNS n)
    (hY : ∀ j a, commutator Y (amplify (τB.gnsStarAlgHom (ρ (M.embedding j a))) n) = 0)
    (r : R) :
    Y.comp (amplify (τB.gnsStarAlgHom (ρ r)) n) =
      (amplify (τB.gnsStarAlgHom (ρ r)) n).comp Y := by
…

    Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify