OAI/Analysis/KadisonKastler/RepresentedProductHomogeneity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Constructed faithful-state homogeneity in every required representation

The modular coisometries give homogeneity on the faithful cyclic tensor representation. A state-preserving spatial equivalence returns it to the original tensor representation, including arbitrary multiplicity.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_spatial_equiv_of_isometric line 25
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_spatial_equiv_of_amplified_isometric line 39
  3. theorem OAI.KadisonKastler.faithfulStateHomogeneity_of_spatial_equiv line 52
  4. theorem OAI.KadisonKastler.PointedMatrixSites.spatial_state_homogeneity line 70
  5. theorem OAI.KadisonKastler.PointedMatrixSites.exists_faithful_product_spatial_equiv line 94
  6. theorem OAI.KadisonKastler.PointedMatrixSites.represented_state_homogeneity line 117
  7. theorem OAI.KadisonKastler.PointedMatrixSites.constructed_represented_expected_matrix_subfactor line 131