OAI/Analysis/KadisonKastler/AmplifiedAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A concrete infinite amplification

The amplification of a corner algebra is the commutant of its diagonally represented commutant. Its matrix entries are exactly the operators in the corner algebra. This construction uses the actual countable matrix units.

  1. theorem OAI.KadisonKastler.FullMatrixCorner.norm_partialDiagonal_apply_le line 23
  2. theorem OAI.KadisonKastler.FullMatrixCorner.norm_partialDiagonal_le line 41
  3. theorem OAI.KadisonKastler.FullMatrixCorner.entry_column line 46
  4. theorem OAI.KadisonKastler.FullMatrixCorner.inflateHom_commute_entry line 52
  5. theorem OAI.KadisonKastler.FullMatrixCorner.inner_matrixEntry line 61
  6. theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_inflate_mul line 65
  7. theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_mul_inflate line 78
  8. theorem OAI.KadisonKastler.FullMatrixCorner.ext_matrixEntry line 89
  9. def OAI.KadisonKastler.FullMatrixCorner.amplifiedAlgebra line 98

    Source documentation

    The concrete amplification in the coordinates supplied by F.

    def amplifiedAlgebra (M : VonNeumannAlgebra E) : VonNeumannAlgebra H where
…
  10. theorem OAI.KadisonKastler.FullMatrixCorner.mem_amplifiedAlgebra_iff_commute line 106
  11. theorem OAI.KadisonKastler.FullMatrixCorner.mem_amplifiedAlgebra_iff line 121

    Source documentation

    Matrix-entry membership characterizes the concrete amplification.

    theorem mem_amplifiedAlgebra_iff (M : VonNeumannAlgebra E) (T : H →L[ℂ] H) :
    T ∈ F.amplifiedAlgebra M ↔ ∀ i j, F.matrixEntry T i j ∈ M := by
…
  12. theorem OAI.KadisonKastler.FullMatrixCorner.entry_mem_amplifiedAlgebra line 136
  13. theorem OAI.KadisonKastler.FullMatrixCorner.inflate_mem_amplifiedAlgebra line 142