OAI/Analysis/BoundedHochschild/MultimodularNormalReduction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The established normal-cocycle reduction retains multimodularity. This is preparatory support for the properly infinite application; it assumes no complete bound on the initial cocycle.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.MultimodularAt.sub line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularOver_iff_at line 22
  3. lemma OAI.BoundedHochschild.KadisonRingrose.normalFirst_eq_normalAt_zero line 31
  4. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_firstNormalCorrection line 43
  5. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_firstNormalRemainder line 56
  6. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_slotInsertion line 61
  7. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularAt_slotRemainder line 66
  8. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularOver_firstNormalRemainder line 71
  9. lemma OAI.BoundedHochschild.KadisonRingrose.multimodularOver_slotRemainder line 77
  10. lemma OAI.BoundedHochschild.KadisonRingrose.normal_before_multimodular line 83
  11. theorem OAI.BoundedHochschild.KadisonRingrose.normal_reduction_multimodular line 112