OAI/Analysis/KadisonKastler/StatePolarSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

State-preserving symmetries commute with polar conjugation

The bounded middle operator is injective. Its core formula and the already constructed resolvent transport identify the polar conjugation on the dense algebraic orbit, without assuming modular uniqueness.

  1. theorem OAI.KadisonKastler.tomitaMiddleOperator_injective line 20
  2. theorem OAI.KadisonKastler.stateSymmetry_middle line 32
  3. theorem OAI.KadisonKastler.stateSymmetry_polar line 47