OAI/Analysis/KadisonSimilarity/Representation/NonunitalRangeRepresentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A nonunital representation of a unital C-star algebra becomes unital on the range of the image of its unit. This also covers the zero fibers used outside a conull spectral base.

  1. def OAI.KadisonSimilarity.nonunitalUnitProjection line 15
  2. theorem OAI.KadisonSimilarity.nonunitalUnitProjection_isStarProjection line 17
  3. theorem OAI.KadisonSimilarity.nonunitalUnitProjection_commutes line 21
  4. def OAI.KadisonSimilarity.nonunitalRangeRepresentation line 26
  5. theorem OAI.KadisonSimilarity.nonunitalRangeRepresentation_coe line 60