OAI/GroupTheory/SimpleAmenable/Simplicial/DiagonalComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EilenbergZilber.bisimplicialMap line 14
2. lemma OAI.EilenbergZilber.level_homology_isIso line 17
3. def OAI.NerveHomotopy.cylinder line 42
4. def OAI.NerveHomotopy.homotopyMap line 45
5. lemma OAI.NerveHomotopy.homotopyMap_zero line 48
6. lemma OAI.NerveHomotopy.homotopyMap_one line 57
7. def OAI.NerveHomotopy.ofNatTrans line 67
8. def OAI.NerveHomotopy.homologyIso line 77
9. instance OAI.NerveHomotopy.homologyMap_isIso line 94
10. abbrev OAI.SimplicialDiagonal.I line 106
11. def OAI.SimplicialDiagonal.uncurry line 107
12. def OAI.SimplicialDiagonal.diagonal line 109
13. def OAI.SimplicialDiagonal.rowIso line 115
14. theorem OAI.SimplicialDiagonal.homologyMap_comp_iso line 120
15. theorem OAI.SimplicialDiagonal.row_homologyMap_isIso line 127
16. lemma OAI.SimplicialDiagonal.homologyMap_isIso line 142
17. def OAI.SimplicialDiagonal.nerveDiagonal line 147
18. lemma OAI.SimplicialDiagonal.nerveDiagonal_isIso line 149