OAI/Analysis/BoundedHochschild/FiniteGroupCochainAverages.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Contractive finite-group averaging on cochains. Every boundary between inputs is averaged independently; the resulting cochain satisfies the ordinary module identities over the linear span of the unitary group.

  1. def OAI.BoundedHochschild.KadisonRingrose.unitaryBimultiply line 16
  2. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryBimultiply_apply line 20
  3. def OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple line 25
  4. def OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport line 28
  5. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_apply line 33
  6. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_norm line 41
  7. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_add line 57
  8. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_smul line 63
  9. def OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransportCLM line 69
  10. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransportCLM_apply line 79
  11. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_comp line 82
  12. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage line 96
  13. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_norm line 100
  14. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_invariant line 114