OAI/Analysis/KadisonKastler/PureCommutingCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compression to a pure cyclic representation

A pure vector-state restriction makes every commuting operator scalar after compression to the cyclic subspace. This is the factorization step for the initial product state on the two commuting factor algebras.

  1. theorem OAI.KadisonKastler.irreducible_commutant_complex_scalar line 22
  2. theorem OAI.KadisonKastler.cyclicGNSMap_intertwines line 48
  3. theorem OAI.KadisonKastler.pureVector_commuting_factorization line 59