OAI/GroupTheory/SimpleAmenable/Homology/ExactShapeHomology.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactShapeHomology.A line 13
  2. abbrev OAI.ExactShapeHomology.c line 14
  3. def OAI.ExactShapeHomology.complex line 16
  4. def OAI.ExactShapeHomology.injection line 22
  5. def OAI.ExactShapeHomology.cocone line 25
  6. def OAI.ExactShapeHomology.isColimit line 34
  7. def OAI.ExactShapeHomology.evaluationHomology line 36
  8. def OAI.ExactShapeHomology.colimitHomology line 39
  9. lemma OAI.ExactShapeHomology.homology_injection line 42
  10. lemma OAI.ExactShapeHomology.evaluationHomology_naturality line 48
  11. def OAI.ExactShapeHomology.homologyCocone line 57
  12. def OAI.ExactShapeHomology.homologyIsColimit line 69
  13. instance OAI.ExactShapeHomology.homology_preserves line 93
  14. instance OAI.ExactShapeHomology.sset_homology_preserves line 98
  15. def OAI.ComponentCoproduct.diagram line 112
  16. def OAI.ComponentCoproduct.cocone line 114
  17. def OAI.ComponentCoproduct.lift line 116
  18. lemma OAI.ComponentCoproduct.lift_forget line 120
  19. lemma OAI.ComponentCoproduct.inclusion_injective line 122
  20. def OAI.ComponentCoproduct.pointwiseIsColimit line 133
  21. def OAI.ComponentCoproduct.isColimit line 150
  22. def OAI.ComponentCoproduct.homologyIsColimit line 152
  23. def OAI.ComponentCoproduct.homologyIso line 155