OAI/Analysis/BoundedHochschild/CountableMatrixHomotopy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit countable matrix average induces the identity in bounded Hochschild cohomology. The uniform finite-group bar bounds allow its homotopy to pass through the fixed weak-star ultralimit.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_homotopy line 20
  2. theorem OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_cocycle line 34