ModularConjugationData.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The modular conjugation data used in preparing a pair

For a cyclic separating vector, Tomita--Takesaki gives J M J = M′. The vector identity J(r* Ω) = r Ω is needed only for elements in the vector-state centralizer. It is not imposed on the whole algebra.

structure OAI.KadisonKastler.ModularConjugationData line 18
theorem OAI.KadisonKastler.ModularConjugationData.right_mem line 33
Source documentation
The full commutant theorem supplies the right inclusion for every subalgebra, without requiring a trace on the source algebra.
```
theorem right_mem (hRM : R ≤ M) (r : Algebra R) :
    conjugationOperator d.conjugation r.val ∈ M.commutant := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator
theorem OAI.KadisonKastler.ModularConjugationData.common_vector line 41
Source documentation
Only centralization of the vector state on the common subalgebra is needed for the right-vector identity in graph comparison.
```
theorem common_vector (hRM : R ≤ M)
    (hcentral : ∀ r : Algebra R, ∀ x : Algebra M,
      inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω))
    (r : Algebra R) :
    conjugationOperator d.conjugation (star r.val) Ω = r.val Ω :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator