OAI/Analysis/BoundedHochschild/CentralPrimitives.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Central cut primitives and restriction through expected embeddings.

  1. lemma OAI.BoundedHochschild.central_differential_values line 30
  2. lemma OAI.BoundedHochschild.norm_sum_supported_cochains line 41
  3. theorem OAI.BoundedHochschild.primitive_of_central_pieces line 59
  4. def OAI.BoundedHochschild.centralOutput line 109
  5. lemma OAI.BoundedHochschild.centralOutput_apply line 112
  6. lemma OAI.BoundedHochschild.norm_centralOutput_le line 115
  7. theorem OAI.BoundedHochschild.primitive_of_central_cut_primitives line 124
  8. structure OAI.BoundedHochschild.ExpectedEmbedding line 168
  9. def OAI.BoundedHochschild.ExpectedEmbedding.restrict line 183
  10. def OAI.BoundedHochschild.ExpectedEmbedding.extend line 186
  11. lemma OAI.BoundedHochschild.ExpectedEmbedding.restrict_apply line 189
  12. lemma OAI.BoundedHochschild.ExpectedEmbedding.extend_apply line 191
  13. lemma OAI.BoundedHochschild.ExpectedEmbedding.restrict_norm line 194
  14. lemma OAI.BoundedHochschild.ExpectedEmbedding.extend_norm line 201
  15. lemma OAI.BoundedHochschild.ExpectedEmbedding.merge_include line 208
  16. lemma OAI.BoundedHochschild.ExpectedEmbedding.differential_restrict line 217
  17. lemma OAI.BoundedHochschild.ExpectedEmbedding.restrict_cocycle line 223
  18. lemma OAI.BoundedHochschild.ExpectedEmbedding.differential_extend_on_include line 231
  19. theorem OAI.BoundedHochschild.ExpectedEmbedding.finite_exactness line 239