SpatialRightSlice.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Right-leg slices and the relative commutant of a product centralizer

def OAI.KadisonKastler.leftTensorVector line 20
Source documentation
Insert a fixed vector in the first tensor leg.
```
def leftTensorVector (ξ : H) : K →L[ℂ] SpatialHilbert H K :=
…
```
theorem OAI.KadisonKastler.leftTensorVector_apply line 25
def OAI.KadisonKastler.rightTensorSlice line 29
Source documentation
Compression in the first leg, with values in operators on the second.
```
def rightTensorSlice (ξ : H) :
    (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) →ₗ[ℂ] (K →L[ℂ] K) where
…
```
theorem OAI.KadisonKastler.rightTensorSlice_apply line 37
theorem OAI.KadisonKastler.spatialRight_leftTensorVector line 41
theorem OAI.KadisonKastler.leftTensorVector_adjoint_spatialRight line 47

theorem OAI.KadisonKastler.spatialRight_commutes_product line 59

Source documentation

A second-leg commutant element commutes with the entire spatial product.

theorem spatialRight_commutes_product (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K)
    (b : K →L[ℂ] K) (hb : b ∈ D.commutant)
    (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) (hT : T ∈ spatialProductAlgebra M D) :
    spatialRight b * T = T * spatialRight b := by
…

Mentions: OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.spatialRight

theorem OAI.KadisonKastler.rightTensorSlice_commute line 107
Source documentation
Right-leg compression intertwines any second-leg operator commuting with the operator being compressed.
```
theorem rightTensorSlice_commute (ξ : H)
    (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K) (b : K →L[ℂ] K)
    (hc : spatialRight b * T = T * spatialRight b) :
    b * rightTensorSlice ξ T = rightTensorSlice ξ T * b := by
…
```
Mentions: OAI.KadisonKastler.spatialRight, OAI.KadisonKastler.rightTensorSlice

theorem OAI.KadisonKastler.rightTensorSlice_mem line 130

Source documentation

Slicing the actual spatial product lands in its second algebra.

theorem rightTensorSlice_mem (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K)
    (ξ : H) (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (hT : T ∈ spatialProductAlgebra M D) : rightTensorSlice ξ T ∈ D := by
…

Mentions: OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.rightTensorSlice

theorem OAI.KadisonKastler.rightTensorSlice_scalar_of_local_swaps line 140

Source documentation

Irreducibility of the product-state centralizer scalarizes every right-leg compression of an operator in its spatial relative commutant.

theorem rightTensorSlice_scalar_of_local_swaps
    (M : VonNeumannAlgebra H) {D : VonNeumannAlgebra K} {Ω : K}
    (L : LocalProductSwaps D Ω) (hΩ : ‖Ω‖ = 1)
    (hsep : Function.Injective (algebraVectorMap D Ω))
    (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (hT : T ∈ spatialProductAlgebra M D)
    (hcomm : ∀ u : unitary (K →L[ℂ] K), (u : K →L[ℂ] K) ∈ D →
      ProductStateCentralizes D Ω u → spatialRight (u : K →L[ℂ] K) * T =
        T * spatialRight (u : K →L[ℂ] K)) (ξ : H) :
    ∃ z : ℂ, rightTensorSlice ξ T = z • (1 : K →L[ℂ] K) := by
…

Mentions: OAI.KadisonKastler.LocalProductSwaps, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.ProductStateCentralizes, OAI.KadisonKastler.spatialRight, OAI.KadisonKastler.rightTensorSlice