SpatialSliceRecovery.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Recovering the first tensor leg from scalar opposite slices

Polarization proves the relative-commutant identity needed for the fixed product factor. No spatial tensor commutation theorem is added as an input.

theorem OAI.KadisonKastler.spatialTensor_vector_ext line 24

Source documentation

Pure-tensor inner products determine a vector in the completed tensor product.

theorem spatialTensor_vector_ext {v w : SpatialHilbert H K}
    (h : ∀ (x : H) (η : K),
      inner ℂ (((x ⊗ₜ[ℂ] η : H ⊗[ℂ] K) : SpatialHilbert H K)) v =
      inner ℂ (((x ⊗ₜ[ℂ] η : H ⊗[ℂ] K) : SpatialHilbert H K)) w) : v = w := by
…

theorem OAI.KadisonKastler.operator_eq_of_diagonal line 39

theorem OAI.KadisonKastler.spatial_eq_left_of_scalar_right_slices line 48

Source documentation

Scalar right-leg slices force an operator to lie entirely in the first leg.

theorem spatial_eq_left_of_scalar_right_slices
    (T : SpatialHilbert H K →L[ℂ] SpatialHilbert H K)
    (Ω : K) (hΩ : ‖Ω‖ = 1)
    (hscalar : ∀ x : H, ∃ z : ℂ, rightTensorSlice x T = z • (1 : K →L[ℂ] K)) :
    T = spatialLeft (K := K) (tensorVectorSlice Ω T) := by
…

Mentions: OAI.KadisonKastler.rightTensorSlice, OAI.KadisonKastler.spatialLeft, OAI.KadisonKastler.tensorVectorSlice

theorem OAI.KadisonKastler.spatial_relative_commutant_of_local_swaps line 95

Source documentation

The first-leg relative-commutant identity for the product-state centralizer follows from local swaps and concrete vector slices.

theorem spatial_relative_commutant_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)) :
    ∃ a ∈ M, T = spatialLeft (K := K) a := by
…

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

theorem OAI.KadisonKastler.scalarCenter_spatialProduct_of_local_swaps line 113
Source documentation
Tensoring a factor with the product algebra remains factorial. This uses the proved relative-commutant identity rather than a tensor-factor classification assumption.
```
theorem scalarCenter_spatialProduct_of_local_swaps
    (M : VonNeumannAlgebra H) (hM : ScalarCenter M)
    {D : VonNeumannAlgebra K} {Ω : K}
    (L : LocalProductSwaps D Ω) (hΩ : ‖Ω‖ = 1)
    (hsep : Function.Injective (algebraVectorMap D Ω)) :
    ScalarCenter (spatialProductAlgebra M D) := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.LocalProductSwaps, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.spatialProductAlgebra