PairedFactor.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The concrete factor in the paired diagonal representation

The two finite traces identify every strong limit of paired operators. Consequently the paired range equals its bicommutant, and the source factor is isomorphic to this actual concrete von Neumann algebra.

def OAI.KadisonKastler.pairedFactorHom line 27
Source documentation
The actual paired representation on the two-fold Hilbert sum.
```
def pairedFactorHom (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N) :
    Algebra M →⋆ₐ[ℂ] (Generator.FiniteHilbert (Fin 2) H →L[ℂ]
      Generator.FiniteHilbert (Fin 2) H) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.Generator.FiniteHilbert
theorem OAI.KadisonKastler.pairedFactorHom_apply_zero line 33
theorem OAI.KadisonKastler.pairedFactorHom_apply_one line 40
theorem OAI.KadisonKastler.pairedFactorHom_injective line 47

theorem OAI.KadisonKastler.pairedFactorHom_range_strong_closed line 59

Source documentation

A strong limit of paired operators is again paired. The trace tests are finite sums of vector coefficients, so no uniform norm bound is needed.

theorem pairedFactorHom_range_strong_closed
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
    (hτM : FiniteVectorTrace τM) (hτN : FiniteVectorTrace τN)
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    {I : Type*} {l : Filter I} [l.NeBot] (a : I → Algebra M)
    (T : Generator.FiniteHilbert (Fin 2) H →L[ℂ] Generator.FiniteHilbert (Fin 2) H)
    (hT : ∀ ξ, Tendsto (fun i => pairedFactorHom θ (a i) ξ) l (𝓝 (T ξ))) :
    T ∈ (pairedFactorHom θ).range := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.Generator.FiniteHilbert, OAI.KadisonKastler.pairedFactorHom

theorem OAI.KadisonKastler.pairedFactorHom_bicommutant line 137

def OAI.KadisonKastler.pairedVonNeumann line 158

Source documentation

The actual von Neumann algebra on the original two-fold Hilbert sum.

def pairedVonNeumann
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N) :
    VonNeumannAlgebra (Generator.FiniteHilbert (Fin 2) H) where
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.Generator.FiniteHilbert

def OAI.KadisonKastler.pairedFactorEquiv line 169

Source documentation

The source algebra is isomorphic to its concrete paired image.

def pairedFactorEquiv
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (θ : Algebra M ≃⋆ₐ[ℂ] Algebra N) :
    Algebra M ≃⋆ₐ[ℂ] Algebra (pairedVonNeumann hM hN θ) :=
…

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

theorem OAI.KadisonKastler.pairedFactorEquiv_apply line 176
theorem OAI.KadisonKastler.pairedVonNeumann_isII1 line 184

theorem OAI.KadisonKastler.complete_closeness_of_finiteFactor_equiv line 210

Source documentation

Uniform closeness of an isomorphism between concrete finite factors is complete closeness, with the paired factor constructed above.

theorem complete_closeness_of_finiteFactor_equiv [TopologicalSpace.SeparableSpace H]
    (hpub : PublishedTracialUltrapower.{u})
    (hmat : PublishedFiniteMatrixUltraproduct)
    (hind : PublishedPopaFiniteBaseIndependence.{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