OAI/Analysis/KadisonKastler/RepresentedProductBicentralizer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The constructed product state in the original representation

The faithful cyclic tensor representation embeds in countable amplification. A commutant unitary returns it to the original space, and a support isometry makes its vector cyclic without changing the state.

  1. theorem OAI.KadisonKastler.equivOfEq_operator line 30
  2. theorem OAI.KadisonKastler.faithfulTensorEquiv_intertwines line 37
  3. theorem OAI.KadisonKastler.PointedMatrixSites.exists_represented_scalar_bicentralizer line 52
  4. theorem OAI.KadisonKastler.PointedMatrixSites.represented_expected_matrix_subfactor line 87