OAI/Analysis/BoundedHochschild/MatrixSectionAveraging.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite unitary group for each matrix section. The choices are independent of the cochain and its degree, so their averages form maps of the Hochschild complex.

  1. structure OAI.BoundedHochschild.KadisonRingrose.MatrixSectionGroup line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionGroup_nonempty line 31
  3. def OAI.BoundedHochschild.KadisonRingrose.matrixSectionGroup line 53
  4. def OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage line 57
  5. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_norm line 62
  6. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_module line 67
  7. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_add line 73
  8. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_smul line 79
  9. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_differential line 85
  10. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionAverage_cocycle line 91