OAI/Analysis/KadisonKastler/SimpleCommutingProductState.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Product states for commuting simple C-star algebras

First extend a pure state and use its scalar commutant compression. Two successive GNS compressions then prescribe arbitrary states on both algebras. Only the simplicity and faithful embedding of the two algebras are required.

  1. theorem OAI.KadisonKastler.state_gns_injective_of_simple line 21
  2. theorem OAI.KadisonKastler.exists_product_state_of_commuting_simple line 33