CenterTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of the concrete centre

Conjugating a represented algebra conjugates its concrete centre by the same unitary. In particular, moving aligned centres back gives a literal common centre for the resulting pair.

theorem OAI.KadisonKastler.mem_concreteCenter_iff line 19
theorem OAI.KadisonKastler.unitaryConj_mem_concreteCenter line 24

theorem OAI.KadisonKastler.Conjugates.concreteCenter line 42

Source documentation

The same implementing unitary transports both algebra and centre.

theorem Conjugates.concreteCenter {M N : VonNeumannAlgebra H}
    {w : unitary (H →L[ℂ] H)} (hw : Conjugates w M N) :
    Conjugates w (concreteCenter M) (concreteCenter N) := by
…

Mentions: OAI.KadisonKastler.Conjugates

theorem OAI.KadisonKastler.concreteCenter_unitaryConjugateAlgebra line 52
theorem OAI.KadisonKastler.concreteCenter_conjugated_neighbor_eq line 64
Source documentation
Moving back a centre-aligning unitary produces exactly equal centres.
```
theorem concreteCenter_conjugated_neighbor_eq {M N : VonNeumannAlgebra H}
    (w : unitary (H →L[ℂ] H))
    (hw : Conjugates w (concreteCenter M) (concreteCenter N)) :
    concreteCenter (unitaryConjugateAlgebra (star w) N) = concreteCenter M := by
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.concreteCenter, OAI.KadisonKastler.unitaryConjugateAlgebra