TracialModularResolution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Tracial specialization of the constructed modular operators

For a tracial vector state the group is the identity on a dense algebra orbit. Its normalization clause is therefore unconditional. The polar conjugation acts by adjoint and gives the right multiplication operators.

theorem OAI.KadisonKastler.tomitaPolarConjugation_tracial line 26
Source documentation
The polar conjugation is adjoint on every tracial algebra vector.
```
theorem tomitaPolarConjugation_tracial (a : Algebra M) :
    tomitaPolarConjugation J Ω hsep hcyc (a.val Ω) = star a.val Ω :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.tomitaPolarConjugation
theorem OAI.KadisonKastler.tomitaPolarConjugation_right_action line 31
Source documentation
In the tracial case the conjugate left action is right multiplication.
```
theorem tomitaPolarConjugation_right_action (a b : Algebra M) :
    conjugationOperator (tomitaPolarConjugation J Ω hsep hcyc) a.val (b.val Ω) =
      (b.val * star a.val) Ω := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tomitaPolarConjugation
theorem OAI.KadisonKastler.tomitaPolarConjugation_tracial_mem_commutant line 43
Source documentation
These right actions commute with the entire represented algebra.
```
theorem tomitaPolarConjugation_tracial_mem_commutant (a : Algebra M) :
    conjugationOperator (tomitaPolarConjugation J Ω hsep hcyc) a.val ∈ M.commutant := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tomitaPolarConjugation
theorem OAI.KadisonKastler.modularStrongGroup_tracial line 65
Source documentation
A faithful tracial cyclic representation has the trivial modular group.
```
theorem modularStrongGroup_tracial (t : Multiplicative ℝ) :
    modularStrongGroup J Ω hsep hcyc t = 1 := by
…
```
Mentions: OAI.KadisonKastler.modularStrongGroup
def OAI.KadisonKastler.tracialModularSpectralResolution line 77