CompressedBicommutant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compressing a represented bicommutant

Commutation of zero extensions of the original commutant suffices to recover the original von Neumann algebra after compression. The operator being compressed need not be supported on the range of the isometry.

theorem OAI.KadisonSimilarity.adjoint_isometricExtension_apply line 23
Source documentation
Applying the isometry's adjoint to a zero extension intertwines the extended operator with the original one.
```
theorem adjoint_isometricExtension_apply (T : H →L[ℂ] H) (y : K) :
    J.toContinuousLinearMap.adjoint (isometricExtension J T y) =
      T (J.toContinuousLinearMap.adjoint y) := by
…
```
Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.compression_commutes_of_isometricExtension_commutes line 34

Source documentation

A commutation relation with a zero extension compresses without any range-support assumption on the other operator.

theorem compression_commutes_of_isometricExtension_commutes
    (T : H →L[ℂ] H) (Q : K →L[ℂ] K)
    (hcomm : isometricExtension J T * Q = Q * isometricExtension J T) :
    T * (J.toContinuousLinearMap.adjoint.comp (Q.comp J.toContinuousLinearMap)) =
      (J.toContinuousLinearMap.adjoint.comp (Q.comp J.toContinuousLinearMap)) * T := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension

theorem OAI.KadisonSimilarity.compression_mem_of_extended_commutant line 49

Source documentation

If the extended original commutant commutes with a represented algebra, its represented bicommutant compresses into the original algebra.

theorem compression_mem_of_extended_commutant
    (P : VonNeumannAlgebra H) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K))
    (hcomm : ∀ T : H →L[ℂ] H, T ∈ P.commutant →
      ∀ a : A, isometricExtension J T * σ a = σ a * isometricExtension J T)
    (Q : K →L[ℂ] K) (hQ : Q ∈ representationVonNeumannAlgebra σ) :
    J.toContinuousLinearMap.adjoint.comp (Q.comp J.toContinuousLinearMap) ∈ P := by
…

Mentions: OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.representationVonNeumannAlgebra