VectorStateTracialRepresentation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Recognizing a faithful tracial vector state

The expected finite algebra in the modular argument already has a faithful trace represented by the common vector. This yields the tracial matrix injectivity theorem directly in that representation.

def OAI.KadisonKastler.tracialRepresentationOfVectorState line 25
Source documentation
A faithful vector trace supplies precisely the concrete tracial representation data.
```
def tracialRepresentationOfVectorState (τ : FaithfulTracialState (Algebra M))
    (Ω : H) (hΩ : ∀ a : Algebra M, τ.toLinearMap a = inner ℂ Ω (a.val Ω)) :
    TracialRepresentation M where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.isInjective_matrix_closure_of_vector_state line 47
Source documentation
A matrix closure carrying a faithful vector trace is injective without an AFD input.
```
theorem isInjective_matrix_closure_of_vector_state
    (τ : FaithfulTracialState (Algebra M)) (Ω : H)
    (hΩ : ∀ a : Algebra M, τ.toLinearMap a = inner ℂ Ω (a.val Ω))
    (A : ℕ → Generator.FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    IsInjective (Generator.FiniteMatrixStage.generatedVonNeumann A) :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.Generator.FiniteMatrixStage, OAI.KadisonKastler.IsInjective, OAI.Generator.FiniteMatrixStage.generatedVonNeumann

theorem OAI.KadisonKastler.isInjective_matrix_closure_of_generated_vector_state line 56

Source documentation

The trace need only be defined on the generated matrix closure.

theorem isInjective_matrix_closure_of_generated_vector_state
    (A : ℕ → Generator.FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (τ : FaithfulTracialState (Algebra (Generator.FiniteMatrixStage.generatedVonNeumann A)))
    (Ω : H) (hΩ : ∀ a, τ.toLinearMap a = inner ℂ Ω (a.val Ω)) :
    IsInjective (Generator.FiniteMatrixStage.generatedVonNeumann A) := by
…

Mentions: OAI.Generator.FiniteMatrixStage, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.Generator.FiniteMatrixStage.generatedVonNeumann, OAI.KadisonKastler.IsInjective

theorem OAI.KadisonKastler.trace_vector_of_expected_state line 68

Source documentation

A unital left-module expectation identifies its trace on the subalgebra with the restriction of the represented expected state.

theorem trace_vector_of_expected_state {N : VonNeumannAlgebra H} (hNM : N ≤ M)
    (τ : FaithfulTracialState (Algebra N)) (P : Algebra M →L[ℂ] Algebra N)
    (hP : P 1 = 1)
    (hleft : ∀ (r : Algebra N) (x : Algebra M),
      P (StarSubalgebra.inclusion hNM r * x) = r * P x)
    (Ω : H) (hΩ : ∀ x : Algebra M, expectedTrace τ P x = inner ℂ Ω (x.val Ω)) :
    ∀ r : Algebra N, τ.toLinearMap r = inner ℂ Ω (r.val Ω) := by
…

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