OAI/Analysis/KadisonKastler/RelativeMatrixSpatial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatially identifying a type III factor with its matrix relative algebra

The isometry onto one matrix corner gives a finite Cuntz family in the factor. Its conjugate family lies in the commutant. Changing between the two families spatially implements the corner-amplification isomorphism.

  1. def OAI.KadisonKastler.cornerIsometryFamily line 24
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_matrix_spatial_equiv line 55
  3. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_matrix_spatial line 90