OAI/Analysis/BoundedHochschild/CompletelyBoundedMapSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The complex vector space of completely bounded maps. No completeness or choice of a particular complete norm is needed for the averaging projection.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_zero line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_smul line 19
  3. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBounded_mono line 27
  4. def OAI.BoundedHochschild.KadisonRingrose.completelyBoundedSubmodule line 32
  5. abbrev OAI.BoundedHochschild.KadisonRingrose.CompletelyBoundedMap line 42
  6. def OAI.BoundedHochschild.KadisonRingrose.completelyBoundedBound line 45
  7. lemma OAI.BoundedHochschild.KadisonRingrose.completelyBoundedBound_spec line 47
  8. def OAI.BoundedHochschild.KadisonRingrose.cbLeftSandwich line 50