OAI/GroupTheory/SimpleAmenable/Simplicial/BarComponents.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntervalBar.Diagram.single_eqToHom line 14
  2. def OAI.IntervalBar.Diagram.componentSimplex line 15
  3. lemma OAI.IntervalBar.Diagram.componentSimplex_iso line 24
  4. def OAI.IntervalBar.Diagram.skeletonSimplex line 30
  5. lemma OAI.IntervalBar.Diagram.skeletonSimplex_mk line 33
  6. lemma OAI.IntervalBar.Diagram.componentSimplex_reindex line 35
  7. lemma OAI.IntervalBar.Diagram.skeletonSimplex_natural line 38
  8. lemma OAI.IntervalBar.Diagram.skeletonSimplex_injective line 43
  9. lemma OAI.IntervalBar.Diagram.skeletonSimplex_surjective line 56
  10. def OAI.IntervalBar.Diagram.skeletonSimplexEquiv line 65
  11. def OAI.IntervalBar.Diagram.componentsZeroIso line 68
  12. lemma OAI.IntervalBar.Diagram.componentsZeroIso_natural line 77
  13. def OAI.IntervalBar.Diagram.componentRowIso line 93
  14. def OAI.IntervalBar.Diagram.componentRowChainIso line 97
  15. def OAI.FilteredNerve.diagram line 110
  16. def OAI.FilteredNerve.cocone line 111
  17. def OAI.FilteredNerve.lastCocone line 115
  18. def OAI.FilteredNerve.lift line 121
  19. lemma OAI.FilteredNerve.lift_forget line 123
  20. lemma OAI.FilteredNerve.lift_map line 124
  21. def OAI.FilteredNerve.pointwiseIsColimit line 141
  22. def OAI.FilteredNerve.isColimit line 154
  23. lemma OAI.FilteredNerve.terminal_acyclic line 156
  24. instance OAI.FilteredNerve.connected line 166
  25. lemma OAI.FilteredNerve.positive_acyclic line 182