OAI/GroupTheory/SimpleAmenable/Simplicial/StringBarNaturality.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SimplicialDiagonal.diagonal_obj_map_apply line 8
  2. lemma OAI.SimplicialDiagonal.diagonal_map_app_apply line 11
  3. lemma OAI.SimplicialDiagonal.nerveDiagonal_obj_map_apply line 14
  4. lemma OAI.SimplicialDiagonal.nerveDiagonal_map_app_apply line 18
  5. lemma OAI.IntervalBar.Diagram.bar₃Map_app_apply line 25
  6. lemma OAI.RestrictedNerve.stringBarRows_map_app_apply line 35
  7. lemma OAI.RestrictedNerve.stringBarTotal_map_apply line 40
  8. lemma OAI.RestrictedNerve.outerResolutionRows_map_app_apply line 48
  9. lemma OAI.RestrictedNerve.middleResolutionRows_map_app_apply line 53
  10. lemma OAI.RestrictedNerve.innerResolutionRows_map_app_apply line 58
  11. lemma OAI.RestrictedNerve.tripleDiagramHorizontal_map_apply line 62
  12. lemma OAI.RestrictedNerve.innerResolutionTotal_map_apply line 73
  13. lemma OAI.RestrictedNerve.middleResolutionTotal_map_apply line 86
  14. lemma OAI.RestrictedNerve.outerResolutionTotal_map_apply line 99
  15. def OAI.RestrictedNerve.stringBarTotalIso line 112
  16. def OAI.RestrictedNerve.stringBarAugmentation line 126
  17. instance OAI.RestrictedNerve.stringBarAugmentation_isIso line 129
  18. def OAI.SimpleAmenable.PolygonObject.stringBarAugmentation line 140
  19. instance OAI.SimpleAmenable.PolygonObject.stringBarAugmentation_isIso line 145