MatrixSubfactorTransfer.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The matrix amplification of an included subfactor acts entrywise. Commutation with the original subfactor therefore gives commutation with the full matrix subfactor on the square array of standard copies.

def OAI.KadisonSimilarity.matrixEntryHom line 19
Source documentation
The entrywise amplification of the actual subfactor embedding.
```
def matrixEntryHom : CStarMatrix (Fin n) (Fin n) A →⋆ₐ[ℂ]
    CStarMatrix (Fin n) (Fin n) B :=
…
```
theorem OAI.KadisonSimilarity.matrixEntryHom_apply line 29
theorem OAI.KadisonSimilarity.matrixEntryHom_injective line 32
theorem OAI.KadisonSimilarity.normalizedMatrixTrace_entryHom line 39
theorem OAI.KadisonSimilarity.matrixEntryHom_cornerProjection line 48
Source documentation
The common scalar matrix units belong to the included matrix subfactor.
```
theorem matrixEntryHom_cornerProjection (i : Fin n) :
    matrixEntryHom φ (matrixCornerProjection (A := A) i) =
…
```
Mentions: OAI.KadisonSimilarity.matrixEntryHom, OAI.KadisonSimilarity.matrixCornerProjection
theorem OAI.KadisonSimilarity.matrixLeftArray_row line 61
Source documentation
The array action can be read as a finite sum of operators on whole rows.
```
theorem matrixLeftArray_row (X : CStarMatrix (Fin n) (Fin n) B)
    (ξ : MatrixGNSArray τ n) (i : Fin n) :
    matrixLeftArray τ X ξ i = ∑ k, amplify (τ.gnsStarAlgHom (X i k)) n (ξ k) := by
…
```
Mentions: OAI.KadisonSimilarity.MatrixGNSArray, OAI.KadisonSimilarity.matrixLeftArray, OAI.KadisonSimilarity.amplify

theorem OAI.KadisonSimilarity.matrix_array_commutes_subfactor line 69

Source documentation

Entrywise commutation gives the full matrix-subfactor commutation.

theorem matrix_array_commutes_subfactor
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (hY : ∀ a : A, Y.comp (amplify (τ.gnsStarAlgHom (φ a)) n) =
      (amplify (τ.gnsStarAlgHom (φ a)) n).comp Y)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    (amplify Y n).comp (matrixLeftArray τ (matrixEntryHom φ X)) =
      (matrixLeftArray τ (matrixEntryHom φ X)).comp (amplify Y n) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixLeftArray, OAI.KadisonSimilarity.matrixEntryHom

theorem OAI.KadisonSimilarity.matrix_gns_commutes_subfactor line 90

Source documentation

The same commutation holds on the actual normalized matrix GNS space.

theorem matrix_gns_commutes_subfactor
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (hY : ∀ a : A, Y.comp (amplify (τ.gnsStarAlgHom (φ a)) n) =
      (amplify (τ.gnsStarAlgHom (φ a)) n).comp Y)
    (X : CStarMatrix (Fin n) (Fin n) A) :
    (matrixGNSLiftOperator τ Y).comp
      ((normalizedMatrixTrace τ n).gnsStarAlgHom (matrixEntryHom φ X)) =
    ((normalizedMatrixTrace τ n).gnsStarAlgHom (matrixEntryHom φ X)).comp
      (matrixGNSLiftOperator τ Y) := by
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.matrixGNSLiftOperator, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.matrixEntryHom

theorem OAI.KadisonSimilarity.matrix_gns_all_small_corners line 108

Source documentation

Projection comparison in the matrix subfactor extends the one-row estimate to every projection of trace at most one over the matrix size.

theorem matrix_gns_all_small_corners
    [PartialOrder A] [StarOrderedRing A]
    (τA : A →ₚ[ℂ] ℂ) (hA : τA 1 = 1)
    (comparison : FiniteFactorProjectionComparison
      (fun X : CStarMatrix (Fin n) (Fin n) A => (normalizedMatrixTrace τA n X).re))
    (Y : HilbertCopies τ.GNS n →L[ℂ] HilbertCopies τ.GNS n)
    (hY : ∀ a : A, Y.comp (amplify (τ.gnsStarAlgHom (φ a)) n) =
      (amplify (τ.gnsStarAlgHom (φ a)) n).comp Y)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hbound : ∀ b : B, ‖commutator Y (amplify (τ.gnsStarAlgHom b) n)‖ ≤ ε * ‖b‖)
    (f : CStarMatrix (Fin n) (Fin n) A) (hf : IsStarProjection f)
    (ht : (normalizedMatrixTrace τA n f).re ≤ (n : ℝ)⁻¹) :
…

Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.normalizedMatrixTrace, OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.commutator