OAI/GroupTheory/SimpleAmenable/Simplicial/StageSimplicialColimit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.degreeRowsStage line 15
  2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.degreeRowsCocone line 24
  3. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.degreeHomologyIsColimit line 31
  4. instance OAI.SimplicialDiagonal.diagonal_preserves line 60
  5. lemma OAI.SimplicialDiagonal.isIso_of_colimit_fac line 66
  6. def OAI.SimplicialDiagonal.diagonalHomologyIsColimit line 76
  7. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.degreeBarHomologyIsColimit line 112
  8. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.middleRowsStage line 118
  9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.middleRowsCocone line 131
  10. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.middleBarHomologyIsColimit line 141
  11. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.topRowsStage line 147
  12. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.topRowsCocone line 160
  13. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.tripleBarHomologyIsColimit line 171