OAI/Analysis/TracialCohomology/HilbertFactorization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Hilbert factorization for bounded Hochschild cohomology.

  1. structure OAI.HochschildNormalPart.SharedHilbertFactor line 22
  2. def OAI.HochschildNormalPart.SharedHilbertFactorizationGoal line 33
  3. lemma OAI.BoundedHochschild.firstRemainder_before_normal line 45
  4. lemma OAI.BoundedHochschild.firstRemainder_before_unitZero line 59
  5. lemma OAI.BoundedHochschild.slot_step_from_factor_data line 67
  6. theorem OAI.BoundedHochschild.normal_before_from_factors line 82
  7. lemma OAI.BoundedHochschild.penultimateSlice_eq_sliceAt line 107
  8. lemma OAI.BoundedHochschild.all_normal_of_before_penultimate line 125
  9. def OAI.BoundedHochschild.SeparatelyNormal line 141
  10. lemma OAI.BoundedHochschild.separatelyNormal_iff_slices line 148
  11. theorem OAI.BoundedHochschild.normal_reduction_from_factor_data line 160
  12. def OAI.BoundedHochschild.BilinearNormalPartPreservation line 180
  13. def OAI.BoundedHochschild.bilinearCochain line 184
  14. lemma OAI.BoundedHochschild.bilinearCochain_apply line 187
  15. lemma OAI.BoundedHochschild.bilinearCochain_firstSlice line 190
  16. lemma OAI.BoundedHochschild.bilinearCochain_normalLast line 196
  17. lemma OAI.BoundedHochschild.bilinear_preservation_iff line 202
  18. lemma OAI.BoundedHochschild.normalAt_old_slice_of_preservation line 223
  19. lemma OAI.BoundedHochschild.normalAt_before_normal_of_preservation line 245
  20. lemma OAI.BoundedHochschild.slot_step_of_preservation line 258
  21. theorem OAI.BoundedHochschild.normal_before_of_preservation line 272
  22. theorem OAI.BoundedHochschild.normal_reduction_of_bilinear_preservation line 296
  23. def OAI.BoundedHochschild.AnalyticProducerGoal line 313