OAI/Analysis/KadisonSimilarity/Representation/ConcreteStandardEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normal standard embedding is proved when the faithful finite trace is supplied by a separating vector in the concrete representation.

  1. theorem OAI.KadisonSimilarity.normal_standard_embedding_of_concrete_trace line 19

    Source documentation

    A concrete faithful vector trace supplies the standard representation embedding, including countable multiplicity, with no separate Hiai input.

    theorem normal_standard_embedding_of_concrete_trace
    (M : VonNeumannAlgebra H)
    [IsClosed (M.toStarSubalgebra : Set (H →L[ℂ] H))]
    (υ : TracialRepresentation M) (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (hτ : ∀ a, τ a = υ.trace a) :
    HiaiNormalStandardEmbeddingInput τ M.toStarSubalgebra.subtype := by
…

    Mentions: OAI.KadisonSimilarity.HiaiNormalStandardEmbeddingInput