OAI/Analysis/BoundedHochschild/MatrixScalarColumns.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Diagonal copies of the proved isometry columns inside finite matrix algebras. These supply the row estimates at every matrix level.

  1. def OAI.BoundedHochschild.KadisonRingrose.matrixScalarHom line 17

    Source documentation

    The unital diagonal embedding into a finite matrix algebra.

    def matrixScalarHom (k : ℕ) : M →⋆ₐ[ℂ] CStarMatrix (Fin k) (Fin k) M where
…
  2. lemma OAI.BoundedHochschild.KadisonRingrose.matrixScalarHom_apply line 31
  3. def OAI.BoundedHochschild.KadisonRingrose.matrixScalarPartialIso line 36
  4. lemma OAI.BoundedHochschild.KadisonRingrose.matrixScalarPartialIso_initial line 42
  5. lemma OAI.BoundedHochschild.KadisonRingrose.matrixScalarPartialIso_final line 46
  6. lemma OAI.BoundedHochschild.KadisonRingrose.matrixScalar_columns line 50