MatrixClosureVectorTrace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The faithful vector trace on a centralizing matrix closure

Finite strong approximation transfers the centralizer identity from the matrix stages to their generated algebra. No trace on the ambient algebra is used.

theorem OAI.KadisonKastler.matrixClosure_vector_centralizes line 22

Source documentation

Centrality of the vector functional passes to the generated matrix algebra.

theorem matrixClosure_vector_centralizes
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) (Ω : H)
    (hcentral : ∀ n a, a ∈ (A n).units.concreteAlgebra → ∀ x : Algebra M,
      inner ℂ Ω ((a * x.val) Ω) = inner ℂ Ω ((x.val * a) Ω))
    (r : Algebra (FiniteMatrixStage.generatedVonNeumann A)) (x : Algebra M) :
    inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω) := by
…

Mentions: OAI.KadisonKastler.Algebra

def OAI.KadisonKastler.faithfulVectorTrace line 69

Source documentation

A faithful unit vector which is tracial on an algebra gives its faithful trace.

def faithfulVectorTrace (N : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hsep : ∀ a : Algebra N, a.val Ω = 0 → a = 0)
    (htr : ∀ a b : Algebra N,
      inner ℂ Ω ((a * b).val Ω) = inner ℂ Ω ((b * a).val Ω)) :
    FaithfulTracialState (Algebra N) where
…

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

def OAI.KadisonKastler.matrixClosureVectorTrace line 96

Source documentation

The trace on the closure is the restriction of the given faithful vector state.

def matrixClosureVectorTrace
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hsep : ∀ a : Algebra M, a.val Ω = 0 → a = 0)
    (hcentral : ∀ n a, a ∈ (A n).units.concreteAlgebra → ∀ x : Algebra M,
      inner ℂ Ω ((a * x.val) Ω) = inner ℂ Ω ((x.val * a) Ω)) :
    FaithfulTracialState (Algebra (FiniteMatrixStage.generatedVonNeumann A)) :=
…

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

theorem OAI.KadisonKastler.matrixClosureVectorTrace_apply line 110