OAI/Analysis/BoundedHochschild/CountableMatrixCorners.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The diagonal corner of the von Neumann algebra generated by a countable matrix system is abelian. The proof uses diagonal operators and weak-star closed commutation relations.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_commute line 22
  2. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_coefficient_central line 56
  3. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixClosure_diagonal_abelian line 79