OAI/Analysis/BoundedHochschild/NormalMultimodularity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Input normalization respects the usual module identities. Only left and right multiplication are needed for this naturality statement.

  1. def OAI.BoundedHochschild.KadisonRingrose.multiplyBoth line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.multiplyBoth_apply line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.multiplyBoth_normal line 22
  4. def OAI.BoundedHochschild.KadisonRingrose.cochainSandwich line 27
  5. lemma OAI.BoundedHochschild.KadisonRingrose.cochainSandwich_apply line 31
  6. lemma OAI.BoundedHochschild.KadisonRingrose.sandwich_update line 35
  7. lemma OAI.BoundedHochschild.KadisonRingrose.sandwich_slice line 41
  8. lemma OAI.BoundedHochschild.KadisonRingrose.normalAt_value line 50
  9. lemma OAI.BoundedHochschild.KadisonRingrose.normalAt_cochainSandwich line 58
  10. lemma OAI.BoundedHochschild.KadisonRingrose.cochainSandwich_leftInput line 76
  11. lemma OAI.BoundedHochschild.KadisonRingrose.cochainSandwich_rightInput line 85
  12. lemma OAI.BoundedHochschild.KadisonRingrose.cochainSandwich_leftOutput line 94
  13. lemma OAI.BoundedHochschild.KadisonRingrose.cochainSandwich_rightOutput line 98
  14. lemma OAI.BoundedHochschild.KadisonRingrose.normalAt_multimodularAt line 102
  15. lemma OAI.BoundedHochschild.KadisonRingrose.normalAt_multimodularOver line 134