OAI/Analysis/KadisonKastler/SpatialReducingProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reducing projections after tensoring the faithful cyclic representation

The entries of a projection commuting with the countable diagonal algebra belong to the original commutant. After tensoring, those entries commute with the whole spatial product, not only its algebraic generators.

  1. theorem OAI.KadisonKastler.countableSpatial_commutes line 24
  2. theorem OAI.KadisonKastler.faithfulCyclic_projection_commutes line 46
  3. theorem OAI.KadisonKastler.faithfulCyclic_tensor_projection_commutes line 63