OAI/Analysis/BoundedHochschild/FiniteGroupCochainChainMap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The contractive finite-group cochain averages commute with the Hochschild differential. No homotopy or cohomology-class assertion is assumed in this calculation.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_add line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_smul line 21
  3. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverageLinear line 26
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_sum line 31
  5. def OAI.BoundedHochschild.KadisonRingrose.leftFaceLinear line 36
  6. def OAI.BoundedHochschild.KadisonRingrose.rightFaceLinear line 41
  7. def OAI.BoundedHochschild.KadisonRingrose.middleFaceLinear line 46
  8. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_face line 52
  9. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_leftCoboundary line 66
  10. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_rightCoboundary line 73
  11. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_middleCoboundary line 82
  12. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_differential line 89
  13. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_cocycle line 99