OAI/Algebra/GroupRing/VertexCollapse.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.VertexCollapse.vertexPath line 17
2. def OAI.TorsionFreeZeroDivisors.VertexCollapse.vertices line 19
3. lemma OAI.TorsionFreeZeroDivisors.VertexCollapse.vertices_zero line 22
4. lemma OAI.TorsionFreeZeroDivisors.VertexCollapse.vertices_one line 24
5. def OAI.TorsionFreeZeroDivisors.VertexCollapse.graph line 25
6. lemma OAI.TorsionFreeZeroDivisors.VertexCollapse.graph_zero line 28
7. lemma OAI.TorsionFreeZeroDivisors.VertexCollapse.graph_vertex line 30
8. def OAI.TorsionFreeZeroDivisors.VertexCollapse.map line 34

   Source documentation

   Homotope an actual map on the whole presentation complex so that EVERY vertex goes to one basepoint. Both cell layers are extended, not collapsed by an unproved quotient/homotopy-equivalence assertion.

   def map : C(CellPresentation.Cover s a,Y) :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.CellPresentation.Cover

9. def OAI.TorsionFreeZeroDivisors.VertexCollapse.homotopy line 36
10. lemma OAI.TorsionFreeZeroDivisors.VertexCollapse.map_vertex line 38