TracialGraphClosability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A separating tracial vector makes the cyclic graph closable. Testing against its dense commutant orbit proves this directly on the closed graph.

theorem OAI.KadisonSimilarity.tracial_cyclic_graph_closable line 22

Source documentation

A tracial cyclic source and a target subrepresentation inside a common normal representation have a closable orbit map if the source identity vector separates that normal algebra.

theorem tracial_cyclic_graph_closable
    (G : TracialCornerGeometry A H)
    (ρ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (π : A →⋆ₐ[ℂ] (E →L[ℂ] E))
    (M : VonNeumannAlgebra E) (hπ : ∀ a, π a ∈ M)
    (I : H →ₗᵢ[ℂ] E) (J : K →ₗᵢ[ℂ] E)
    (hI : ∀ a, I.toContinuousLinearMap.comp (G.left a) =
      (π a).comp I.toContinuousLinearMap)
    (hJ : ∀ a, J.toContinuousLinearMap.comp (ρ a) =
      (π a).comp J.toContinuousLinearMap)
    (hsep : ∀ a : M.toStarSubalgebra, (a : E →L[ℂ] E) (I (G.vector 1)) = 0 → a = 0)
    (ξ : K) :
    ∀ x : cyclicGraph G.left ρ (G.vector 1) ξ,
…

Mentions: OAI.KadisonSimilarity.TracialCornerGeometry, OAI.KadisonSimilarity.cyclicGraph

theorem OAI.KadisonSimilarity.countable_embedding_of_separating_trace_vector line 95

Source documentation

Assemble the cyclic embeddings when the source trace vector is separating in the target's normal algebra.

theorem countable_embedding_of_separating_trace_vector
    [TopologicalSpace.SeparableSpace E]
    (G : TracialCornerGeometry A H) (π : A →⋆ₐ[ℂ] (E →L[ℂ] E))
    (M : VonNeumannAlgebra E) (hπ : ∀ a, π a ∈ M)
    (I : H →ₗᵢ[ℂ] E)
    (hI : ∀ a, I.toContinuousLinearMap.comp (G.left a) =
      (π a).comp I.toContinuousLinearMap)
    (hsep : ∀ a : M.toStarSubalgebra, (a : E →L[ℂ] E) (I (G.vector 1)) = 0 → a = 0) :
    ∃ U : E →ₗᵢ[ℂ] CountableCopies H, ∀ a,
      U.toContinuousLinearMap.comp (π a) =
        (countableAmplify (G.left a)).comp U.toContinuousLinearMap := by
…

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