OAI/Analysis/BoundedHochschild/MatrixAmplification.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Isometric matrix amplification from unital isometry columns

The actual C*-matrix algebra is identified with the original algebra by compression and reconstruction. Consequently matrix norms can be used directly in the remaining completely bounded argument.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.column_star_mul line 25
  2. def OAI.BoundedHochschild.KadisonRingrose.columnCompression line 33

    Source documentation

    The matrix of an element with respect to unital isometry columns.

    def columnCompression (a : M) : CStarMatrix (Fin n) (Fin n) M :=
…
  3. def OAI.BoundedHochschild.KadisonRingrose.columnReconstruction line 37

    Source documentation

    Reconstruction from the actual matrix entries.

    def columnReconstruction (A : CStarMatrix (Fin n) (Fin n) M) : M :=
…
  4. lemma OAI.BoundedHochschild.KadisonRingrose.columnReconstruction_compression line 41
  5. lemma OAI.BoundedHochschild.KadisonRingrose.columnCompression_reconstruction line 59
  6. lemma OAI.BoundedHochschild.KadisonRingrose.columnCompression_mul line 76
  7. def OAI.BoundedHochschild.KadisonRingrose.columnMatrixEquiv line 93

    Source documentation

    The compression/reconstruction identification preserves the C*-norm.

    def columnMatrixEquiv : M ≃⋆ₐ[ℂ] CStarMatrix (Fin n) (Fin n) M where
…
  8. lemma OAI.BoundedHochschild.KadisonRingrose.columnCompression_norm line 116