OAI/Analysis/BoundedHochschild/CountableMatrixProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The countable matrix average fixes multimodular cochains and is therefore an idempotent contraction commuting with the differential.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_fixes line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_fixes line 25
  3. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixAverage_idempotent line 39