OAI/Analysis/BoundedHochschild/NormalCochainTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Unitary transport and finite cochain averaging preserve separate normality. Normalizing an input also commutes with unitary transport.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTuple_update line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.inputTransport line 28
  3. def OAI.BoundedHochschild.KadisonRingrose.outputTransport line 33
  4. lemma OAI.BoundedHochschild.KadisonRingrose.inputTransport_normal line 37
  5. lemma OAI.BoundedHochschild.KadisonRingrose.outputTransport_normal line 43
  6. lemma OAI.BoundedHochschild.KadisonRingrose.transport_updateSlice line 48
  7. lemma OAI.BoundedHochschild.KadisonRingrose.cochainUnitaryTransport_normal line 57
  8. lemma OAI.BoundedHochschild.KadisonRingrose.separatelyNormal_smul line 69
  9. lemma OAI.BoundedHochschild.KadisonRingrose.separatelyNormal_sum line 83
  10. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage_normal line 96