MatrixRetractionDescent.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Descending the finite-corner construction

The upper algebras are concrete algebras on a second Hilbert space. An actual UCP retraction of the ambient embedding returns their conjugacy to the original representation. The hypotheses below are the data needed from the crossed-product construction, not a stability assertion about it.

def OAI.KadisonKastler.matrixDescentError line 37
theorem OAI.KadisonKastler.continuous_matrixDescentError line 39
theorem OAI.KadisonKastler.matrixDescentError_zero line 42
theorem OAI.KadisonKastler.matrixDescentError_monotone line 45

theorem OAI.KadisonKastler.spatial_of_retracted_matrix_algebras line 51

Source documentation

The concrete finite-corner conjugacy descends through a UCP retraction whose restriction to the upper target lands in the original target.

theorem spatial_of_retracted_matrix_algebras
    (h : FiniteFactorPublishedInputs.{v})
    (M N : VonNeumannAlgebra H)
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
    (R : (K →L[ℂ] K) →CP (H →L[ℂ] H)) (hR : R 1 = 1)
    (hfix : ∀ x, R (j x) = x)
    (A B S : VonNeumannAlgebra K) (hSA : S ≤ A) (hS : IsInjective S)
    (E : Submodule ℂ K) [CompleteSpace E] (F : FullMatrixCorner E)
    (hFS : ∀ i k, F.entry i k ∈ S)
    (hCorner : Generator.IsII1Factor
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsInjective, OAI.KadisonKastler.FullMatrixCorner, OAI.Generator.IsII1Factor