OAI/Geometry/SingularHomology/SingularAcyclicModels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SingularAcyclicModels.singularFunctor line 13
  2. abbrev OAI.Problem340.SingularAcyclicModels.degree line 16
  3. abbrev OAI.Problem340.SingularAcyclicModels.complex line 21
  4. abbrev OAI.Problem340.SingularAcyclicModels.model line 35
  5. instance OAI.Problem340.SingularAcyclicModels.contractible_model line 37
  6. lemma OAI.Problem340.SingularAcyclicModels.model_exact line 43
  7. def OAI.Problem340.SingularAcyclicModels.liftCycle line 48
  8. lemma OAI.Problem340.SingularAcyclicModels.liftCycle_comp line 64
  9. def OAI.Problem340.SingularAcyclicModels.homotopyZero line 75
  10. def OAI.Problem340.SingularAcyclicModels.homotopyOfDegreeZero line 96
  11. def OAI.Problem340.SingularAcyclicModels.transpose line 100
  12. def OAI.Problem340.SingularAcyclicModels.naturalHomotopy line 109
  13. def OAI.Problem340.SingularAcyclicModels.homotopyApp line 117
  14. lemma OAI.Problem340.SingularAcyclicModels.homotopyApp_naturality line 124
  15. lemma OAI.Problem340.SingularAcyclicModels.homologyMap_eq line 131
  16. def OAI.Problem340.SingularAcyclicModels.operator line 137
  17. def OAI.Problem340.SingularAcyclicModels.operatorHomotopy line 150