OAI/Analysis/BoundedHochschild/CompletelyBoundedPrimitives.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The module projection contracts the Hochschild complex on cochains with uniformly completely bounded last slices. The argument is the one-sided module homotopy underlying completely bounded cohomology vanishing.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.cb_cocycle_last_relation line 15
  2. lemma OAI.BoundedHochschild.KadisonRingrose.averagedLastCochain_differential line 29
  3. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_lastSliceEstimate line 51
  4. theorem OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_primitive_of_lastSliceEstimate line 68