OAI/Geometry/HyperbolicGroups/VoltagePrismGluing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A genuine dimension-two contraction gluing theorem. Its local input is a continuous prism for each face, compatible with the SAME edge prisms.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.faceLift_sheet_injective line 17
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.edgeLift_exists line 27
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.intersection_edge line 39
  4. structure OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.EdgePrisms line 54
  5. structure OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.FacePrism line 62
  6. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.anchoredFacePrism line 73
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.anchoredFacePrism_lift line 78
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.anchoredFacePrism_agree line 88
  9. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.contraction line 113
  10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.contraction_initial line 116
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.contraction_final line 120
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.contraction_edge line 125