SpatialSlice.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete vector slices of the spatial von Neumann product

theorem OAI.KadisonKastler.spatialLeft_tensorVector line 17
theorem OAI.KadisonKastler.tensorVector_adjoint_spatialLeft line 24

theorem OAI.KadisonKastler.spatialLeft_commutes_product line 36

Source documentation

A first-leg commutant element commutes with the entire actual product.

theorem spatialLeft_commutes_product (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K)
    (a : H →L[ℂ] H) (ha : a ∈ M.commutant)
    (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) (hT : T ∈ spatialProductAlgebra M D) :
    spatialLeft a * T = T * spatialLeft a := by
…

Mentions: OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.spatialLeft

theorem OAI.KadisonKastler.tensorVectorSlice_mem line 84
Source documentation
Slicing an element of the spatial product lands in the original first algebra, by the bicommutant theorem.
```
theorem tensorVectorSlice_mem (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K)
    (ξ : K) (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (hT : T ∈ spatialProductAlgebra M D) : tensorVectorSlice ξ T ∈ M := by
…
```
Mentions: OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVectorSlice