SpatialMatrix.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix amplification in a spatial tensor product

An actual matrix-unit system in the second tensor factor gives a star representation of operator-valued matrices. Its norm is the C-star matrix norm: multiplying on both sides by matrix units recovers each coefficient, so the representation is faithful whenever the second Hilbert space is nonzero. No assertion about amplification of an ordinary algebra gap is used here.

def OAI.KadisonKastler.matrixEntryStarHom line 24

def OAI.KadisonKastler.spatialMatrixUnits line 42

Source documentation

Matrix units on the second tensor leg.

def spatialMatrixUnits (E : MatrixUnitSystem ι (K →L[ℂ] K)) :
    MatrixUnitSystem ι (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) :=
…

theorem OAI.KadisonKastler.spatialMatrixUnits_entry line 47
def OAI.KadisonKastler.spatialMatrixCoefficient line 50

def OAI.KadisonKastler.spatialMatrixHom line 59

Source documentation

The actual finite spatial matrix representation.

def spatialMatrixHom (E : MatrixUnitSystem ι (K →L[ℂ] K)) :
    CStarMatrix ι ι (H →L[ℂ] H) →⋆ₐ[ℂ]
      (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) :=
…

theorem OAI.KadisonKastler.spatialMatrixHom_apply line 66
theorem OAI.KadisonKastler.spatialMatrixHom_sandwich line 79
Source documentation
Matrix-unit multiplication extracts a single spatial coefficient.
```
theorem spatialMatrixHom_sandwich (E : MatrixUnitSystem ι (K →L[ℂ] K))
    (X : CStarMatrix ι ι (H →L[ℂ] H)) (o i j : ι) :
    spatialRight (H := H) (E.entry o i) * spatialMatrixHom E X *
…
```
Mentions: OAI.KadisonKastler.spatialRight, OAI.KadisonKastler.spatialMatrixHom
theorem OAI.KadisonKastler.spatialMatrixHom_injective line 106
Source documentation
A nonzero second tensor leg makes the finite matrix representation faithful.
```
theorem spatialMatrixHom_injective (E : MatrixUnitSystem ι (K →L[ℂ] K)) :
    Function.Injective (spatialMatrixHom (H := H) E) := by
…
```
Mentions: OAI.KadisonKastler.spatialMatrixHom
theorem OAI.KadisonKastler.norm_spatialMatrixHom line 131
Source documentation
The representation has exactly the operator-valued C-star matrix norm.
```
theorem norm_spatialMatrixHom (E : MatrixUnitSystem ι (K →L[ℂ] K))
    (X : CStarMatrix ι ι (H →L[ℂ] H)) : ‖spatialMatrixHom E X‖ = ‖X‖ :=
…
```
Mentions: OAI.KadisonKastler.spatialMatrixHom

theorem OAI.KadisonKastler.spatialMatrixHom_mem line 138

Source documentation

If both sets of coefficients belong to the original algebras, their finite spatial sum belongs to the actual spatial product algebra.

theorem spatialMatrixHom_mem (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K)
    (E : MatrixUnitSystem ι (K →L[ℂ] K)) (hE : ∀ i j, E.entry i j ∈ D)
    (X : CStarMatrix ι ι (H →L[ℂ] H)) (hX : ∀ i j, X i j ∈ M) :
    spatialMatrixHom E X ∈ spatialProductAlgebra M D := by
…

Mentions: OAI.KadisonKastler.spatialMatrixHom, OAI.KadisonKastler.spatialProductAlgebra