OAI/Analysis/KadisonKastler/IsometricRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting a representation through a reducing isometry

Compression by an isometry is multiplicative when its range projection commutes with the represented algebra. The intertwining identity is kept explicit for later weak-continuity and faithfulness arguments.

  1. theorem OAI.KadisonKastler.isometry_equiv_comp_projection line 17
  2. theorem OAI.KadisonKastler.isometry_adjoint_apply line 35
  3. def OAI.KadisonKastler.isometricCompression line 39
  4. theorem OAI.KadisonKastler.isometricCompression_intertwines line 42
  5. def OAI.KadisonKastler.isometricRestriction line 52
  6. theorem OAI.KadisonKastler.isometricRestriction_apply line 82