OAI/Analysis/BoundedHochschild/IsometryDefectColumns.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal columns from an isometry defect

A nonunitary isometry supplies countably many equivalent, orthogonal defect projections. This is an algebraic ingredient of the properly infinite case.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.isometry_pow_initial line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.isometry_pow_cancel line 30
  3. def OAI.BoundedHochschild.KadisonRingrose.isometryDefect line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.isometryDefect_projection line 36
  5. lemma OAI.BoundedHochschild.KadisonRingrose.isometryDefect_mul line 44
  6. lemma OAI.BoundedHochschild.KadisonRingrose.isometryDefect_mul_pow_succ line 48
  7. lemma OAI.BoundedHochschild.KadisonRingrose.isometry_column_initial line 52
  8. def OAI.BoundedHochschild.KadisonRingrose.isometryColumn line 60
  9. lemma OAI.BoundedHochschild.KadisonRingrose.isometryColumn_initial line 65
  10. lemma OAI.BoundedHochschild.KadisonRingrose.isometryColumn_coe line 69
  11. lemma OAI.BoundedHochschild.KadisonRingrose.isometryColumn_star_mul_of_lt line 73
  12. lemma OAI.BoundedHochschild.KadisonRingrose.isometryColumn_star_mul_of_ne line 85
  13. lemma OAI.BoundedHochschild.KadisonRingrose.isometryColumn_final_orthogonal line 93