OAI/Analysis/KadisonSimilarity/Representation/CStarCorner.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual unital C-star algebra cut out by a projection. Its identity is the projection, and its norm is the ambient norm.

  1. def OAI.KadisonSimilarity.cstarCornerSubalgebra line 14
  2. instance OAI.KadisonSimilarity.cstarCornerSubalgebra_closed line 32
  3. abbrev OAI.KadisonSimilarity.CStarCorner line 36
  4. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 42) line 42
  5. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 47) line 47
  6. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 49) line 49
  7. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 51) line 51
  8. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 54) line 54
  9. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 56) line 56
  10. instance OAI.KadisonSimilarity.CStarCorner.(instance at line 58) line 58
  11. theorem OAI.KadisonSimilarity.CStarCorner.coe_one line 60
  12. def OAI.KadisonSimilarity.CStarCorner.compress line 66

    Source documentation

    Every ambient compression is an element of the corner.

    def compress (a : P) : CStarCorner e he := ⟨e * a * e, by
…

    Mentions: OAI.KadisonSimilarity.CStarCorner

  13. theorem OAI.KadisonSimilarity.CStarCorner.coe_compress line 73
  14. theorem OAI.KadisonSimilarity.CStarCorner.full line 75