OAI/GroupTheory/SimpleAmenable/Homology/FilteredHomology.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FilteredHomology.A line 11
  2. abbrev OAI.FilteredHomology.c line 12
  3. def OAI.FilteredHomology.complex line 13
  4. def OAI.FilteredHomology.injection line 19
  5. def OAI.FilteredHomology.cocone line 22
  6. def OAI.FilteredHomology.isColimit line 31
  7. def OAI.FilteredHomology.evaluationHomology line 33
  8. def OAI.FilteredHomology.colimitHomology line 36
  9. lemma OAI.FilteredHomology.homology_injection line 39
  10. lemma OAI.FilteredHomology.evaluationHomology_naturality line 45
  11. def OAI.FilteredHomology.homologyCocone line 54
  12. def OAI.FilteredHomology.homologyIsColimit line 68
  13. instance OAI.FilteredHomology.homology_preserves line 93
  14. instance OAI.FilteredHomology.chain_preserves line 105
  15. instance OAI.FilteredHomology.sset_homology_preserves line 111
  16. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.homologyIsColimit line 120
  17. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.barHomologyIsColimit line 124
  18. def OAI.StageProductColimit.powerMap line 137
  19. lemma OAI.StageProductColimit.powerMap_id line 142
  20. lemma OAI.StageProductColimit.powerMap_comp line 143
  21. instance OAI.StageProductColimit.(instance at line 145) line 145
  22. lemma OAI.StageProductColimit.powerMap_injective line 147
  23. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.productStage line 155
  24. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.productCocone line 167
  25. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.productNerveCocone line 175
  26. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.exists_lift_product line 177
  27. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.productNerveIsColimit line 192
  28. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.productHomologyIsColimit line 204