OAI/GroupTheory/SimpleAmenable/Simplicial/PiFiber.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiSSet.nervePiIso line 11
  2. def OAI.ComponentTranslation.base line 22
  3. def OAI.ComponentTranslation.fiberIso line 23
  4. instance OAI.ComponentTranslation.fiber_nonempty line 25
  5. instance OAI.ComponentTranslation.fiber_nerve_connected line 26
  6. def OAI.PiFiber.prod line 39
  7. def OAI.PiFiber.piece line 40
  8. def OAI.PiFiber.diagram line 41
  9. def OAI.PiFiber.inclusion line 42
  10. def OAI.PiFiber.cocone line 44
  11. def OAI.PiFiber.pointwiseIsColimit line 45
  12. def OAI.PiFiber.isColimit line 68
  13. def OAI.PiFiber.homologyIsColimit line 70
  14. def OAI.PiFiber.homologyIso line 73
  15. def OAI.PiFiber.h1PieceIso line 77