OAI/Analysis/BoundedHochschild/BarInsertionFaces.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The elementary Hochschild-face formulas for bounded bar insertions. The finite signed averaging identity is proved separately from these pointwise operator identities.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_leftCoboundary_zero line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_leftCoboundary_succ line 27
  3. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_rightCoboundary_last line 36
  4. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_rightCoboundary_castSucc line 50
  5. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_middleCoboundary_castSucc line 60
  6. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_middleCoboundary_succ line 70
  7. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_middleCoboundary_after line 80
  8. lemma OAI.BoundedHochschild.KadisonRingrose.barInsertion_middleCoboundary_before line 92