MatrixOperatorGeneration.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix algebras and von Neumann generation

These elementary finite-sum arguments are independent of spatial tensor products and perturbation theorems.

def OAI.KadisonKastler.entryMatrixAlgebra line 31
Source documentation
The finite matrices whose entries belong to a specified star algebra.
```
def entryMatrixAlgebra (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    StarSubalgebra ℂ (CStarMatrix ι ι (H →L[ℂ] H)) where
…
```

def OAI.KadisonKastler.matrixOperatorAlgebra line 48

Source documentation

The same finite matrices acting on the finite Hilbert sum.

def matrixOperatorAlgebra (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    StarSubalgebra ℂ (FiniteHilbert ι H →L[ℂ] FiniteHilbert ι H) :=
…

theorem OAI.KadisonKastler.operatorEntry_hilbertMatrix line 54
theorem OAI.KadisonKastler.hilbertMatrix_operatorEntries line 61
theorem OAI.KadisonKastler.mem_matrixOperatorAlgebra_iff line 73
theorem OAI.KadisonKastler.matrixOperatorAlgebra_mono line 85
theorem OAI.KadisonKastler.generated_matrixOperatorAlgebra line 92
Source documentation
Finite matrix amplification commutes with von Neumann generation.
```
theorem generated_matrixOperatorAlgebra (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    generatedVonNeumannAlgebra (matrixOperatorAlgebra (ι := ι) S) =
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.matrixOperatorAlgebra

theorem OAI.KadisonKastler.matrixOperatorAlgebra_iSup line 141

Source documentation

Increasing unions also commute with finite matrix amplification.

theorem matrixOperatorAlgebra_iSup (S : ℕ → StarSubalgebra ℂ (H →L[ℂ] H))
    (hS : Monotone S) :
    matrixOperatorAlgebra (ι := ι) (⨆ n, S n) = ⨆ n, matrixOperatorAlgebra (ι := ι) (S n) := by
…

Mentions: OAI.KadisonKastler.matrixOperatorAlgebra