TraceUnitaryIsomorphism.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-factor isomorphism from boundary unitary images

The unitary image formula determines a continuous unital Jordan map. The reverse distance gives surjectivity, and the two-by-two matrix unitaries force its multiplicative orientation.

theorem OAI.KadisonKastler.exists_near_starEquiv_of_traceDense_unitary_images line 27

Source documentation

A uniformly close unitary-image formula on a trace-dense family produces a nearby star isomorphism between the finite factors.

theorem exists_near_starEquiv_of_traceDense_unitary_images
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (J : Algebra M →ₗ[ℂ] E) (K : Algebra N →ₗ[ℂ] E)
    (hJ : ∀ a, ‖J a‖ = traceTwoNorm τM a)
    (hK : ∀ a, ‖K a‖ = traceTwoNorm τN a)
    (ρ : I → unitary (Algebra M))
    (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
      ∃ i, traceTwoNorm τM ((u : Algebra M) - ρ i) < ε)
    (S : unitary (E →L[ℂ] E)) (hS1 : (S : E →L[ℂ] E) (J 1) = K 1)
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm