NormalStandardEmbedding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The standard embedding of a separable concrete finite algebra is constructed from its faithful normal GNS trace. No vector-realization or standard-embedding result is an additional hypothesis.

theorem OAI.KadisonSimilarity.countable_embedding_of_normal_geometry line 23

Source documentation

A faithful normal tracial geometry supplies a countable standard embedding.

theorem countable_embedding_of_normal_geometry
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    (M : VonNeumannAlgebra H) (G : TracialCornerGeometry M.toStarSubalgebra E)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ) (hτ : ∀ a, τ a = G.trace a)
    (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (N : VonNeumannAlgebra E) (hN : G.left.range = N.toStarSubalgebra) :
    ∃ I : H →ₗᵢ[ℂ] CountableCopies E, ∀ a : M.toStarSubalgebra,
      I.toContinuousLinearMap.comp (a : H →L[ℂ] H) =
        (countableAmplify (G.left a)).comp I.toContinuousLinearMap := by
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.CountableCopies, OAI.KadisonSimilarity.countableAmplify

theorem OAI.KadisonSimilarity.normal_standard_embedding_of_normal_gns line 47

Source documentation

The local Hiai standard-embedding consequence, proved from the faithful normal trace by spectral truncation and cyclic decomposition.

theorem normal_standard_embedding_of_normal_gns
    (M : VonNeumannAlgebra H) (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (h1 : τ 1 = 1) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hf : ∀ a, τ (star a * a) = 0 → a = 0) (hN : HasNormalGNS τ) :
    HiaiNormalStandardEmbeddingInput τ M.toStarSubalgebra.subtype := by
…

Mentions: OAI.KadisonSimilarity.HasNormalGNS, OAI.KadisonSimilarity.HiaiNormalStandardEmbeddingInput