OAI/GroupTheory/FiniteType/SingularPrism.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularPrism.top_h_precomp line 24
  2. lemma OAI.SingularPrism.sset_h_precomp line 29
  3. theorem OAI.SingularPrism.component_precomp line 37
  4. theorem OAI.SingularPrism.prism_precomp line 47
  5. def OAI.SingularChains.start line 78
  6. def OAI.SingularChains.finish line 80
  7. def OAI.SingularChains.cylinderHom line 83
  8. def OAI.SingularChains.prism line 88
  9. def OAI.SingularChains.precompCylinder line 92
  10. lemma OAI.SingularChains.prism_precomp line 95
  11. lemma OAI.SingularChains.prism_boundary_zero line 100
  12. lemma OAI.SingularChains.prism_boundary_succ line 107
  13. structure OAI.SingularNormalization.Coherent line 125
  14. def OAI.SingularNormalization.Coherent.top line 134
  15. lemma OAI.SingularNormalization.Coherent.start_eq line 136
  16. lemma OAI.SingularNormalization.Coherent.top_face line 140
  17. lemma OAI.SingularNormalization.Coherent.hom_face line 145
  18. def OAI.SingularNormalization.Coherent.topComponent line 150
  19. lemma OAI.SingularNormalization.Coherent.top_comm line 153
  20. def OAI.SingularNormalization.Coherent.topMap line 162
  21. def OAI.SingularNormalization.Coherent.prismComponent line 169
  22. lemma OAI.SingularNormalization.Coherent.identity_prism_zero line 172
  23. lemma OAI.SingularNormalization.Coherent.lifted_face_prism line 181
  24. lemma OAI.SingularNormalization.Coherent.identity_prism_succ line 186
  25. lemma OAI.SingularNormalization.Coherent.prism_comm_zero line 200
  26. lemma OAI.SingularNormalization.Coherent.prism_comm_succ line 207
  27. def OAI.SingularNormalization.Coherent.homComponent line 216
  28. lemma OAI.SingularNormalization.Coherent.homComponent_succ line 219
  29. def OAI.SingularNormalization.Coherent.chainHomotopy line 222
  30. def OAI.SingularNormalization.tightening line 239
  31. lemma OAI.SingularNormalization.tightening_top line 246
  32. lemma OAI.SingularNormalization.homologyMap_congr_component line 259
  33. lemma OAI.SingularNormalization.homologyMap_const line 267
  34. lemma OAI.SingularNormalization.tightening_component line 280
  35. theorem OAI.SingularNormalization.homology_isZero_of_low_homotopy line 290