OAI/Analysis/KadisonKastler/CyclicOrbitRestriction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Faithful cyclic restriction to a vector orbit

A separating vector remains separating after restriction to its closed orbit, where it is cyclic by construction. The concrete reducing map retains the commutant-corner identification.

  1. abbrev OAI.KadisonKastler.cyclicOrbitSpace line 21
  2. def OAI.KadisonKastler.cyclicOrbitVector line 23
  3. theorem OAI.KadisonKastler.cyclicOrbitProjection_mem line 25
  4. abbrev OAI.KadisonKastler.cyclicOrbitHom line 30
  5. theorem OAI.KadisonKastler.cyclicOrbitHom_apply line 34
  6. theorem OAI.KadisonKastler.cyclicOrbitHom_separating line 38
  7. theorem OAI.KadisonKastler.cyclicOrbitHom_injective line 46
  8. def OAI.KadisonKastler.cyclicOrbitAlgebra line 52
  9. def OAI.KadisonKastler.cyclicOrbitEquiv line 55
  10. theorem OAI.KadisonKastler.cyclicOrbitEquiv_val line 60
  11. theorem OAI.KadisonKastler.cyclicOrbitAlgebra_separating line 63
  12. theorem OAI.KadisonKastler.cyclicOrbitAlgebra_cyclic line 74
  13. theorem OAI.KadisonKastler.cyclicOrbitAlgebra_commutant line 88