OAI/Analysis/KadisonKastler/ConstructedStateCocycle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A constructed cocycle comparing two faithful cyclic vector states

The two-by-two matrix modular action yields a strongly-star continuous unitary cocycle. Its diagonal restrictions are identified through the actual closed Tomita graphs. Thus the cores of the two constructed modular groups are isomorphic without a change-of-state premise.

  1. def OAI.KadisonKastler.constructedStateCocycle line 28
  2. theorem OAI.KadisonKastler.constructed_state_core_equiv line 50