OAI/Analysis/KadisonKastler/CentralBlockDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Block decomposition from central coordinate projections

Commutation with the coordinate projections gives the diagonal blocks. Conversely, a uniformly bounded family of corner operators belongs to the original algebra by the bicommutant theorem, without a normality assumption.

  1. theorem OAI.KadisonKastler.blockAlgebraDecomposition_of_central_coordinates line 22