OAI/Geometry/HyperbolicGroups/VoltageTriangleContraction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A literal contracting prism on each lifted triangle once its genuine pi2 obstruction is the coboundary of the constructed directed cochain.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdge line 25
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdge_agree line 29
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdge_initial line 35
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdge_final line 38
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedEdge_fixed line 42
  6. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleObstruction line 55
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.triangleLoops_correct line 61
  8. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction line 69
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction_initial line 76
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction_final line 79
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction_bottom line 81
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction_left line 85
  13. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.terminalContraction_right line 89
  14. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle line 94
  15. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle_initial line 97
  16. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle_final line 102
  17. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle_bottom line 106
  18. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle_left line 111
  19. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.correctedTriangle_right line 116