ExpectedCentralizer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A finite expected subfactor gives a centralizing functional

The trace in this construction is only on the finite subfactor. Composing it with a bimodular conditional expectation gives a functional on the ambient algebra which centralizes that subfactor. No traciality of the ambient algebra is asserted or used.

def OAI.KadisonKastler.expectedTrace line 23
Source documentation
The functional obtained by composing a finite trace and an expectation.
```
def expectedTrace (τ : FaithfulTracialState A) (E : B →L[ℂ] A) : B →L[ℂ] ℂ :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.expectedTrace_apply line 27
theorem OAI.KadisonKastler.norm_expectedTrace_le line 30
theorem OAI.KadisonKastler.expectedTrace_one line 36
theorem OAI.KadisonKastler.expectedTrace_restrict line 40

theorem OAI.KadisonKastler.expectedTrace_centralizes line 46

Source documentation

Bimodularity and the finite trace imply the centralizer identity.

theorem expectedTrace_centralizes (τ : FaithfulTracialState A) (E : B →L[ℂ] A)
    (ι : A →⋆ₐ[ℂ] B)
    (hleft : ∀ a x, E (ι a * x) = a * E x)
    (hright : ∀ a x, E (x * ι a) = E x * a) (a : A) (x : B) :
    expectedTrace τ E (ι a * x) = expectedTrace τ E (x * ι a) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.expectedTrace

theorem OAI.KadisonKastler.vector_functional_centralizes_of_expectation line 60

Source documentation

When the composed state is represented by a vector, its centralizer identity is exactly the identity required by the matrix-state argument.

theorem vector_functional_centralizes_of_expectation
    (M R : VonNeumannAlgebra H) (hRM : R ≤ M)
    (τ : FaithfulTracialState (Algebra R))
    (E : Algebra M →L[ℂ] Algebra R)
    (hleft : ∀ (r : Algebra R) (x : Algebra M),
      E (StarSubalgebra.inclusion hRM r * x) = r * E x)
    (hright : ∀ (r : Algebra R) (x : Algebra M),
      E (x * StarSubalgebra.inclusion hRM r) = E x * r)
    (Ω : H)
    (hΩ : ∀ x : Algebra M, expectedTrace τ E x = inner ℂ Ω (x.val Ω))
    (r : Algebra R) (x : Algebra M) :
    inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.expectedTrace

theorem OAI.KadisonKastler.norm_vector_of_expectedTrace line 78

Source documentation

A normalized expectation and a representing vector force unit norm.

theorem norm_vector_of_expectedTrace
    (M R : VonNeumannAlgebra H) (τ : FaithfulTracialState (Algebra R))
    (E : Algebra M →L[ℂ] Algebra R) (hE : E 1 = 1) (Ω : H)
    (hΩ : ∀ x : Algebra M, expectedTrace τ E x = inner ℂ Ω (x.val Ω)) :
    ‖Ω‖ = 1 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.expectedTrace