OAI/Analysis/BoundedHochschild/BarDifferential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bar-complex identities and the square-zero Hochschild differential.

  1. lemma OAI.BoundedHochschild.mergeInputs_mergeInputs line 28
  2. def OAI.BoundedHochschild.barDifferential line 45
  3. lemma OAI.BoundedHochschild.barDifferential_squared line 48
  4. lemma OAI.BoundedHochschild.mergeInputs_cons_zero line 89
  5. lemma OAI.BoundedHochschild.mergeInputs_cons_succ line 96
  6. def OAI.BoundedHochschild.barEnvelope line 105
  7. lemma OAI.BoundedHochschild.barEnvelope_apply line 108
  8. lemma OAI.BoundedHochschild.barDifferential_envelope_apply line 118
  9. lemma OAI.BoundedHochschild.barDifferential_envelope line 139
  10. theorem OAI.BoundedHochschild.differential_squared line 153
  11. lemma OAI.BoundedHochschild.differential_is_cocycle line 160