OAI/GroupTheory/SimpleAmenable/Simplicial/CoefficientNaturality.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoefficientNerve.comp_pair line 12
  2. lemma OAI.CoefficientNerve.square_of_components line 19
  3. lemma OAI.CoefficientNerve.iso_transport_cancel line 27
  4. def OAI.CoefficientNerve.mapNat line 37
  5. lemma OAI.CoefficientNerve.single_mapNat line 44
  6. lemma OAI.CoefficientNerve.mapNat_id line 46
  7. lemma OAI.CoefficientNerve.mapNat_comp line 51
  8. lemma OAI.CoefficientNerve.post_natural line 59
  9. def OAI.CoefficientNerve.functor line 70
  10. instance OAI.CoefficientNerve.(instance at line 75) line 75
  11. def OAI.CoefficientNerve.vertices line 82
  12. def OAI.CoefficientNerve.degree line 84
  13. def OAI.CoefficientNerve.vertexCocone line 86
  14. def OAI.CoefficientNerve.vertexIsColimit line 89
  15. def OAI.CoefficientNerve.degreeIso line 93
  16. instance OAI.CoefficientNerve.degree_preservesLimits line 105
  17. instance OAI.CoefficientNerve.degree_preservesColimits line 107
  18. def OAI.CoefficientNerve.levelMap line 116
  19. lemma OAI.CoefficientNerve.levelMap_id line 119
  20. lemma OAI.CoefficientNerve.levelMap_comp line 122
  21. def OAI.CoefficientNerve.chainSimplicial line 126
  22. def OAI.CoefficientNerve.chainSimplicialHomology line 136
  23. def OAI.CoefficientNerve.double line 147
  24. def OAI.CoefficientNerve.rowIso line 149