MatrixVonNeumannRange.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The concrete von Neumann algebra of finite operator matrices

The commutant of the diagonally amplified commutant consists exactly of operator matrices with entries in the original von Neumann algebra. This constructs the normal matrix realization used by spectral rounding.

def OAI.KadisonSimilarity.matrixOfOperator line 20
Source documentation
The bounded coordinate blocks, packaged as an actual matrix.
```
def matrixOfOperator {n : ℕ} (T : HilbertCopies H n →L[ℂ] HilbertCopies H n) :
    Matrix (Fin n) (Fin n) (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.matrixOfOperator_apply line 25
theorem OAI.KadisonSimilarity.matrixOperator_entryCompressions line 31
Source documentation
Every finite operator array is recovered from its coordinate blocks.
```
theorem matrixOperator_entryCompressions {n : ℕ}
    (T : HilbertCopies H n →L[ℂ] HilbertCopies H n) :
    matrixOperator (matrixOfOperator T) = T := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.matrixOfOperator
theorem OAI.KadisonSimilarity.amplify_single line 47
Source documentation
A diagonal operator acts on a coordinate inclusion by the original operator.
```
theorem amplify_single {n : ℕ} (T : H →L[ℂ] H) (j : Fin n) (x : H) :
    amplify T n (PiLp.single 2 j x) = PiLp.single 2 j (T x) := by
…
```
Mentions: OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.amplify_commutes_iff_entries line 57
Source documentation
Diagonal commutation is equivalent to commutation of every matrix entry.
```
theorem amplify_commutes_iff_entries {n : ℕ} (A : H →L[ℂ] H)
    (T : HilbertCopies H n →L[ℂ] HilbertCopies H n) :
    amplify A n * T = T * amplify A n ↔
      ∀ i j, A * matrixEntryCompression i j T = matrixEntryCompression i j T * A := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixEntryCompression
def OAI.KadisonSimilarity.amplifiedCommutantSet line 83
Source documentation
The diagonal copy of the commutant, viewed just as a set of operators.
```
def amplifiedCommutantSet (P : VonNeumannAlgebra H) (n : ℕ) :
    Set (HilbertCopies H n →L[ℂ] HilbertCopies H n) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
def OAI.KadisonSimilarity.matrixVonNeumann line 88
Source documentation
Finite matrices over P, constructed as an actual double-commutant algebra.
```
def matrixVonNeumann (P : VonNeumannAlgebra H) (n : ℕ) :
    VonNeumannAlgebra (HilbertCopies H n) where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies
theorem OAI.KadisonSimilarity.mem_matrixVonNeumann_iff_commutes line 97
Source documentation
The extra star tests in the centralizer are redundant for this set.
```
theorem mem_matrixVonNeumann_iff_commutes (P : VonNeumannAlgebra H) {n : ℕ}
    (T : HilbertCopies H n →L[ℂ] HilbertCopies H n) :
    T ∈ matrixVonNeumann P n ↔ ∀ A ∈ P.commutant, amplify A n * T = T * amplify A n := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.matrixVonNeumann, OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.mem_matrixVonNeumann_iff_entries line 111
Source documentation
Membership is exactly entrywise membership in the original algebra.
```
theorem mem_matrixVonNeumann_iff_entries (P : VonNeumannAlgebra H) {n : ℕ}
    (T : HilbertCopies H n →L[ℂ] HilbertCopies H n) :
    T ∈ matrixVonNeumann P n ↔ ∀ i j, matrixEntryCompression i j T ∈ P := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.matrixVonNeumann, OAI.KadisonSimilarity.matrixEntryCompression
theorem OAI.KadisonSimilarity.matrixOperator_mem_matrixVonNeumann_iff line 127
Source documentation
The usual matrix-operator action has exactly the same entrywise criterion.
```
theorem matrixOperator_mem_matrixVonNeumann_iff (P : VonNeumannAlgebra H) {n : ℕ}
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    matrixOperator X ∈ matrixVonNeumann P n ↔ ∀ i j, X i j ∈ P := by
…
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.matrixVonNeumann
theorem OAI.KadisonSimilarity.representedMatrixHom_injective line 137
Source documentation
A faithful representation remains faithful on finite matrices.
```
theorem representedMatrixHom_injective (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hσ : Function.Injective σ) (n : ℕ) : Function.Injective (representedMatrixHom σ n) := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrixHom

theorem OAI.KadisonSimilarity.representedMatrixHom_range line 151

Source documentation

A normal represented range has its actual matrix von Neumann range.

theorem representedMatrixHom_range (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (P : VonNeumannAlgebra H) (hσ : σ.range = P.toStarSubalgebra) (n : ℕ) :
    (representedMatrixHom σ n).range = (matrixVonNeumann P n).toStarSubalgebra := by
…

Mentions: OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.matrixVonNeumann

theorem OAI.KadisonSimilarity.representedMatrixHom_single_one line 181
Source documentation
Scalar matrix units act as the coordinate matrix units.
```
theorem representedMatrixHom_single_one (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    {n : ℕ} (i j : Fin n) :
    representedMatrixHom σ n (CStarMatrix.ofMatrix (Matrix.single i j (1 : A))) =
      copyMatrixUnit i j := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.copyMatrixUnit
theorem OAI.KadisonSimilarity.representedMatrixHom_diagonal line 199
Source documentation
Constant diagonal matrices represent the diagonal amplification.
```
theorem representedMatrixHom_diagonal (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (n : ℕ) (a : A) :
    representedMatrixHom σ n (CStarMatrix.ofMatrix (Matrix.diagonal (fun _ : Fin n => a))) =
      amplify (σ a) n := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.matrixRange_commutant_is_diagonal line 215

Source documentation

A matrix commutant element has one repeated diagonal block, which commutes with the original represented algebra.

theorem matrixRange_commutant_is_diagonal
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) {n : ℕ} [NeZero n]
    (T : HilbertCopies H n →L[ℂ] HilbertCopies H n)
    (hT : T ∈ Set.centralizer ((representedMatrixHom σ n).range :
      Set (HilbertCopies H n →L[ℂ] HilbertCopies H n))) :
    ∃ B : H →L[ℂ] H, T = amplify B n ∧
      B ∈ Set.centralizer (σ.range : Set (H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.amplify_mem_matrixRange_commutant line 241

Source documentation

Every amplified scalar commutant element commutes with the represented matrix algebra.

theorem amplify_mem_matrixRange_commutant
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (n : ℕ) (B : H →L[ℂ] H)
    (hB : B ∈ Set.centralizer (σ.range : Set (H →L[ℂ] H))) :
    amplify B n ∈ Set.centralizer ((representedMatrixHom σ n).range :
      Set (HilbertCopies H n →L[ℂ] HilbertCopies H n)) := by
…

Mentions: OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.HilbertCopies

theorem OAI.KadisonSimilarity.mem_representation_commutant_iff line 256

Source documentation

Taking the scalar bicommutant does not change its commutant.

theorem mem_representation_commutant_iff (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (B : H →L[ℂ] H) :
    B ∈ (representationVonNeumannAlgebra σ).commutant ↔
      B ∈ Set.centralizer (σ.range : Set (H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.representationVonNeumannAlgebra_matrix line 268
Source documentation
Finite matrices commute with passage to the represented bicommutant. This supplies the actual matrix membership needed by Kaplansky density.
```
theorem representationVonNeumannAlgebra_matrix (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H))
    (n : ℕ) [NeZero n] :
    representationVonNeumannAlgebra (representedMatrixHom σ n) =
      matrixVonNeumann (representationVonNeumannAlgebra σ) n := by
…
```
Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.representedMatrixHom, OAI.KadisonSimilarity.matrixVonNeumann

theorem OAI.KadisonSimilarity.matrixOperator_mem_representationVonNeumannAlgebra_iff line 287

Source documentation

Entrywise bicommutant membership for an arbitrary represented algebra.

theorem matrixOperator_mem_representationVonNeumannAlgebra_iff
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) {n : ℕ} [NeZero n]
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    matrixOperator X ∈ representationVonNeumannAlgebra (representedMatrixHom σ n) ↔
      ∀ i j, X i j ∈ representationVonNeumannAlgebra σ := by
…

Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.representedMatrixHom

theorem OAI.KadisonSimilarity.subtype_range_eq line 304
def OAI.KadisonSimilarity.matrixVonNeumannEquiv line 314
Source documentation
The usual C-star matrix algebra over P is star-isomorphic to its constructed concrete von Neumann realization.
```
def matrixVonNeumannEquiv (n : ℕ) [NeZero n] :
    CStarMatrix (Fin n) (Fin n) P.toStarSubalgebra ≃⋆ₐ[ℂ]
      (matrixVonNeumann P n).toStarSubalgebra := by
…
```
Mentions: OAI.KadisonSimilarity.matrixVonNeumann