OAI/Analysis/KadisonKastler/FiniteFactorSpatial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial implementation of the nearby finite-factor isomorphism

The actual paired factor makes uniform amplification applicable on the original Hilbert space. The published commutant-distance input and the proved polar-intertwiner argument then produce the required unitary.

  1. theorem OAI.KadisonKastler.finiteFactor_spatial_of_near_starEquiv line 39

    Source documentation

    A sufficiently close isomorphism between represented finite factors is implemented by a nearby unitary, using the uniform amplification theorem and the precise published commutant-distance input.

    theorem finiteFactor_spatial_of_near_starEquiv
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{u})
    (hFock : PublishedDiagonalFockRepresentation.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    (hCyclic : PublishedCyclicSimilarity.{u, u} (A := Algebra (pairedVonNeumann hM hN θ)))
…

    Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.pairedVonNeumann