CommonPositionFiniteIsomorphism.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-factor isomorphism transferred from common position

The published common-position representation supplies the standard positions and the conjugation estimate. The scalar boundary theorem then constructs an isomorphism, which is transported to the original represented factors with the explicit comparison error.

theorem OAI.KadisonKastler.CommonTracialPositionData.exists_finiteFactor_isomorphism line 32

Source documentation

The common-position and scalar boundary inputs give an isomorphism of the original factors with the full transported estimate.

theorem exists_finiteFactor_isomorphism
    (d : CommonTracialPositionData M N R hRM hRN g K)
    (hBoundary : PublishedBoundary.{u}) (hTom : PublishedFieldTomiyamaFamily K)
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (hirr : ∀ a : Algebra M,
      (∀ r : Algebra R, coordinateInclusion hRM r * a = a * coordinateInclusion hRM r) →
      ∃ c : ℂ, a = c • (1 : Algebra M))
    (hgap : kkDistance M N < g)
    {b : ℝ} (hb : 2 * d.tolerance < b) (hbsmall : b < 1 / 100000) :
    ∃ θ : Algebra M ≃⋆ₐ[ℂ] Algebra N,
      ∀ x, ‖(θ x : H →L[ℂ] H) - (x : H →L[ℂ] H)‖ ≤
…

Mentions: OAI.KadisonKastler.CommonTracialPositionData, OAI.KadisonKastler.PublishedFieldTomiyamaFamily, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance