OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalEquivalence.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.IntervalBar.Diagram.mapFaithful line 17
2. instance OAI.IntervalBar.Diagram.mapFull line 24
3. instance OAI.IntervalBar.Diagram.mapIsEquivalence line 34
4. instance OAI.IntervalBar.Diagram.map₃IsEquivalence line 36
5. def OAI.IntervalBar.Diagram.simplicialMap line 46
6. def OAI.IntervalBar.Diagram.bar line 52
7. def OAI.IntervalBar.Diagram.barMap line 53
8. lemma OAI.IntervalBar.Diagram.barMap_homology_isIso line 56
9. def OAI.SimplicialDiagonal.fromZero line 69
10. lemma OAI.SimplicialDiagonal.fromZero_zero line 79
11. instance OAI.SimplicialDiagonal.diagonal_connected line 84
12. lemma OAI.CategoryTheory.nerve.connected_of_hom line 97
13. instance OAI.IntervalBar.Diagram.zero_nonempty line 107
14. def OAI.IntervalBar.Diagram.zeroHom line 108
15. instance OAI.IntervalBar.Diagram.zero_nerve_connected line 110
16. instance OAI.IntervalBar.Diagram.bar_connected line 112
17. lemma OAI.IntervalBar.Diagram.simplicialMap_reindex_id line 126
18. lemma OAI.IntervalBar.Diagram.simplicialMap_reindex_comp line 132
19. lemma OAI.IntervalBar.Diagram.barMap_reindex_id line 139
20. lemma OAI.IntervalBar.Diagram.barMap_reindex_comp line 142
21. def OAI.IntervalBar.Diagram.rows₂ line 147
22. def OAI.IntervalBar.Diagram.bar₂ line 152
23. instance OAI.IntervalBar.Diagram.bar₂_connected line 153
24. lemma OAI.IntervalBar.Diagram.map_map_reindex line 156