OAI/GroupTheory/SimpleAmenable/Simplicial/BarContractible.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SimplicialDiagonal.connected_of_iso line 13
2. lemma OAI.SimplicialDiagonal.connectivity line 18
3. lemma OAI.CategoryTheory.nerve.const_map line 39
4. lemma OAI.CategoryTheory.nerve.positive_zero line 43
5. instance OAI.IntervalBar.Diagram.zero_thin line 59
6. instance OAI.IntervalBar.Diagram.zero_hom_nonempty line 61
7. instance OAI.IntervalBar.Diagram.hom_thin line 62
8. def OAI.IntervalBar.Diagram.homOfAll line 65
9. lemma OAI.IntervalBar.Diagram.bar_acyclic line 69
10. lemma OAI.IntervalBar.Diagram.zero_bar_acyclic line 81
11. lemma OAI.IntervalBar.Diagram.map_map_reindex_unit_app line 93
12. lemma OAI.IntervalBar.Diagram.map_map_reindex_comp line 104
13. lemma OAI.IntervalBar.Diagram.barMap_map_reindex_id line 146
14. lemma OAI.IntervalBar.Diagram.barMap_map_reindex_comp line 152
15. lemma OAI.IntervalBar.Diagram.bar₂Map_reindex_id line 161
16. lemma OAI.IntervalBar.Diagram.bar₂Map_reindex_comp line 167
17. def OAI.IntervalBar.Diagram.rows₃ line 174
18. def OAI.IntervalBar.Diagram.bar₃ line 179
19. instance OAI.IntervalBar.Diagram.bar₃_connected line 180
20. lemma OAI.IntervalBar.Diagram.bar₂_acyclic line 184
21. lemma OAI.IntervalBar.Diagram.bar₂_H1_zero line 195
22. lemma OAI.IntervalBar.Diagram.bar₃_low_zero line 203