OAI/Analysis/BoundedHochschild/CocycleNormalParts.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Normal corrections and first- and last-input normal cocycles.

  1. def OAI.BoundedHochschild.normalLast line 38
  2. lemma OAI.BoundedHochschild.normalLast_apply line 41
  3. lemma OAI.BoundedHochschild.normalLast_snoc line 44
  4. lemma OAI.BoundedHochschild.normalLast_normal line 48
  5. lemma OAI.BoundedHochschild.normalLast_identity line 58
  6. def OAI.BoundedHochschild.reducedNormalCocycle line 84
  7. def OAI.BoundedHochschild.normalCorrection line 87
  8. lemma OAI.BoundedHochschild.sign_square line 90
  9. lemma OAI.BoundedHochschild.sign_succ line 94
  10. lemma OAI.BoundedHochschild.normal_correction_identity line 98
  11. lemma OAI.BoundedHochschild.reducedNormalCocycle_normal line 122
  12. lemma OAI.BoundedHochschild.differentialValue_sub line 137
  13. lemma OAI.BoundedHochschild.rightCoboundary_differential line 142
  14. lemma OAI.BoundedHochschild.reducedNormalCocycle_cocycle line 151
  15. lemma OAI.BoundedHochschild.normalLast_norm line 168
  16. lemma OAI.BoundedHochschild.rightCoboundary_norm line 177
  17. lemma OAI.BoundedHochschild.insertLast_one_norm line 185
  18. lemma OAI.BoundedHochschild.reducedNormalCocycle_norm line 192
  19. lemma OAI.BoundedHochschild.normalCorrection_norm line 198
  20. theorem OAI.BoundedHochschild.ordinary_to_last_normal line 204
  21. def OAI.BoundedHochschild.reverseArguments line 224
  22. lemma OAI.BoundedHochschild.reverseArguments_apply line 227
  23. lemma OAI.BoundedHochschild.reverseArguments_norm line 230
  24. def OAI.BoundedHochschild.firstSliceN line 233
  25. lemma OAI.BoundedHochschild.firstSliceN_apply line 236
  26. def OAI.BoundedHochschild.normalFirst line 246
  27. lemma OAI.BoundedHochschild.normalFirst_cons line 249
  28. lemma OAI.BoundedHochschild.normalFirst_norm line 254
  29. lemma OAI.BoundedHochschild.normalFirst_normal line 257
  30. lemma OAI.BoundedHochschild.differentialValue_cons line 265
  31. lemma OAI.BoundedHochschild.normalFirst_identity line 283
  32. def OAI.BoundedHochschild.firstNormalCorrectionN line 307
  33. def OAI.BoundedHochschild.firstNormalRemainderN line 310
  34. lemma OAI.BoundedHochschild.firstNormalCorrectionN_apply line 313
  35. lemma OAI.BoundedHochschild.firstNormalRemainderN_apply line 316
  36. lemma OAI.BoundedHochschild.firstNormalRemainderN_cocycle line 330
  37. lemma OAI.BoundedHochschild.firstNormalRemainderN_identity line 335
  38. lemma OAI.BoundedHochschild.firstNormalCorrectionN_norm line 339