TracialInclusionModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous normal representations of a trace-preserving inclusion. The source range is proved closed, retaining the given source algebra.

structure OAI.KadisonSimilarity.TracialInclusionModel line 19

theorem OAI.KadisonSimilarity.exists_tracialInclusionModel line 37

Source documentation

Both given algebras occur as normal ranges on one Hilbert space.

theorem exists_tracialInclusionModel
    {X Y : Type u} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℂ Y] [CompleteSpace Y]
    (eA : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] A) (eB : StrongDual ℂ Y ≃ₗᵢ⋆[ℂ] B)
    (τA : A →ₚ[ℂ] ℂ) (τB : B →ₚ[ℂ] ℂ)
    (hnA : BoundedHochschild.TraceInPredual eA τA)
    (hnB : BoundedHochschild.TraceInPredual eB τB)
    (h1B : τB 1 = 1) (htrB : ∀ a b, τB (a * b) = τB (b * a))
    (hfB : ∀ a, τB (star a * a) = 0 → a = 0)
    (φ : A →⋆ₐ[ℂ] B) (hi : Function.Injective φ)
    (ht : ∀ a, τB (φ a) = τA a) : Nonempty (TracialInclusionModel φ τB) := by
…

Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.KadisonSimilarity.TracialInclusionModel