SpatialAssociator.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The associator of the completed Hilbert tensor product

The algebraic Hilbert tensor associator is isometric. Its two canonical dense embeddings into the completed tensor products therefore extend it to an actual unitary identification of the two parenthesizations.

def OAI.KadisonKastler.tensorDenseEmbedding line 28
theorem OAI.KadisonKastler.tensorDenseEmbedding_tmul line 33
theorem OAI.KadisonKastler.tensorDenseEmbedding_dense line 39
def OAI.KadisonKastler.spatialAssocLeftEmbedding line 73
Source documentation
The algebraic threefold tensor product in the left-associated completion.
```
def spatialAssocLeftEmbedding :
    (H ⊗[ℂ] K) ⊗[ℂ] L →ₗᵢ[ℂ] SpatialHilbert (SpatialHilbert H K) L :=
…
```
def OAI.KadisonKastler.spatialAssocRightEmbedding line 78
Source documentation
The algebraic threefold tensor product in the right-associated completion.
```
def spatialAssocRightEmbedding :
    H ⊗[ℂ] (K ⊗[ℂ] L) →ₗᵢ[ℂ] SpatialHilbert H (SpatialHilbert K L) :=
…
```
theorem OAI.KadisonKastler.spatialAssocLeftEmbedding_dense line 82
theorem OAI.KadisonKastler.spatialAssocRightEmbedding_dense line 86
def OAI.KadisonKastler.spatialAssociator line 91
Source documentation
The canonical associator on completed Hilbert tensor products.
```
def spatialAssociator :
    SpatialHilbert (SpatialHilbert H K) L ≃ₗᵢ[ℂ] SpatialHilbert H (SpatialHilbert K L) :=
…
```
theorem OAI.KadisonKastler.spatialAssociator_embedding line 101
theorem OAI.KadisonKastler.spatialAssociator_tmul line 107
theorem OAI.KadisonKastler.spatialAssociator_symm_tmul line 119

theorem OAI.KadisonKastler.spatialTriple_ext line 132

Source documentation

Equality of bounded operators can be checked on elementary threefold tensors.

theorem spatialTriple_ext
    {A B : SpatialHilbert H (SpatialHilbert K L) →L[ℂ] SpatialHilbert H (SpatialHilbert K L)}
    (h : ∀ x : H, ∀ y : K, ∀ z : L,
      A (((x ⊗ₜ[ℂ] ((y ⊗ₜ[ℂ] z : K ⊗[ℂ] L) : SpatialHilbert K L)) :
        H ⊗[ℂ] SpatialHilbert K L) : SpatialHilbert H (SpatialHilbert K L)) =
      B (((x ⊗ₜ[ℂ] ((y ⊗ₜ[ℂ] z : K ⊗[ℂ] L) : SpatialHilbert K L)) :
        H ⊗[ℂ] SpatialHilbert K L) : SpatialHilbert H (SpatialHilbert K L))) : A = B := by
…

theorem OAI.KadisonKastler.spatialAssociator_conjugate_tensor line 152

Source documentation

Conjugation by the associator reassociates the actual tensor operators.

theorem spatialAssociator_conjugate_tensor
    (a : H →L[ℂ] H) (b : K →L[ℂ] K) (c : L →L[ℂ] L) :
    spatialAssociator.conjStarAlgEquiv (spatialTensorOp (spatialTensorOp a b) c) =
      spatialTensorOp a (spatialTensorOp b c) := by
…