OAI/Analysis/KadisonKastler/NormalSpatialImplementation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial implementation between cyclic separating normal representations

Only the explicitly supplied bounded weak continuity of the representation change is used. The two diagonal vector states need not agree.

  1. theorem OAI.KadisonKastler.exists_spatial_of_normal_cyclic_separating line 24

    Source documentation

    The spatial map is constructed from the two-state matrix algebra and its modular conjugation.

    theorem exists_spatial_of_normal_cyclic_separating
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    (hθ : BoundedWeakNormal M (N.toStarSubalgebra.subtype.comp θ.toStarAlgHom))
    (Ω : H) (ξ : K)
    (hΩc : DenseRange (algebraVectorMap M Ω)) (hξc : DenseRange (algebraVectorMap N ξ))
    (hΩs : Function.Injective (algebraVectorMap M Ω))
    (hξs : Function.Injective (algebraVectorMap N ξ)) :
    ∃ W : H ≃ₗᵢ[ℂ] K, ∀ (a : Algebra M) (x : H), W (a.val x) = (θ a).val (W x) := by
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedWeakNormal, OAI.KadisonKastler.algebraVectorMap