OAI/Analysis/KadisonKastler/PeriodicMatrixUnits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite full matrix algebras from countable matrix units

The finite algebras need not be increasing. Their matrix units agree with the countable matrix units on any fixed finite collection of columns once the matrix size is large enough.

  1. def OAI.KadisonKastler.CuntzFamily.matrixUnits line 21
  2. def OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits line 36
  3. theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_mem line 40
  4. theorem OAI.KadisonKastler.FullMatrixCorner.finiteCuntz_column line 46
  5. theorem OAI.KadisonKastler.FullMatrixCorner.finiteCuntz_adjoint_column line 50
  6. theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_column line 55
  7. theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_agree_on_column line 65