TracialModularCommutant.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The full commutant identity for a tracial cyclic vector

Adjoint on the dense algebra orbit determines adjoint on the commutant orbit as well. Applying the right-action calculation to both algebras and using the bicommutant identity proves equality of the conjugate algebra and the commutant.

theorem OAI.KadisonKastler.conjugation_right_action_of_star_vectors line 19
theorem OAI.KadisonKastler.conjugation_mem_commutant_of_star_vectors line 30
theorem OAI.KadisonKastler.conjugation_star_vectors_commutant line 49
theorem OAI.KadisonKastler.tomitaPolarConjugation_tracial_commutant line 83
theorem OAI.KadisonKastler.tomitaPolarConjugation_tracial_commutant_eq line 89
Source documentation
The exact modular commutant equality, in the tracial case.
```
theorem tomitaPolarConjugation_tracial_commutant_eq :
    conjugateRightAlgebra (tomitaPolarConjugation J Ω hsep hcyc)
      (tomitaPolarConjugation_involutive J Ω hsep hcyc) M = M.commutant := by
…
```
Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.tomitaPolarConjugation, OAI.KadisonKastler.tomitaPolarConjugation_involutive
def OAI.KadisonKastler.tracialModularConjugationData line 107
Source documentation
A tracial state gives modular conjugation data.
```
def tracialModularConjugationData : ModularConjugationData M Ω :=
…
```
Mentions: OAI.KadisonKastler.ModularConjugationData