OAI/Geometry/HyperbolicGroups/EdgeMerge.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide line 21

    Source documentation

    The common side of two distinct, non-monogon faces. These are local incidence hypotheses, not any normalization or genus conclusion.

    structure MergeSide (a b : D) : Prop where
…
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.ne line 30
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.paired_back line 31
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.face_left_ne_right line 32
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.face_right_ne_left line 35
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.edge_invariant line 38
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.crossed_a line 47
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.crossed_b line 48
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.vertex_a line 52
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.vertex_b line 53
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.erase_identity line 61

    Source documentation

    The exact permutation identity underlying deletion of a shared edge: face cycles merge; the two endpoint vertex cycles only bypass the deleted corners. Other contacts between the faces are immaterial.

    lemma erase_identity :
    bypassPair (M.face * swap a b) a b * (swap a b * M.edge) =
      bypassPair M.vertex a b := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.bypassPair

  12. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge line 77

    Source documentation

    Delete the paired sides and join the remaining oriented boundaries. Unlike cancellation of an entire equal pair of cells, this works when the remaining boundaries differ.

    def mergeEdge (h : M.MergeSide a b) : PictureMap {x // OffPair a b x} where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.OffPair

  13. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_vertex line 83
  14. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_faces line 93
  15. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_vertices line 101
  16. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_euler line 108