OAI/Geometry/HyperbolicGroups/EdgeMergeComponents.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.old_face_le_crossed line 22
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.crossed_le_components line 32
  3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative line 38
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_kept line 43
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_a line 46
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_b line 49
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_crossed line 52
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_face line 64
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.representative_edge line 72
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.retained_components line 88
  11. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.MergeSide.component_card line 100

    Source documentation

    No component is created or lost by deleting a common side of distinct faces, even when their boundaries also touch elsewhere.

    theorem component_card : Nat.card (Quotient (M.mergeEdge h).components) = Nat.card (Quotient M.components) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components

  12. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_genusZero line 129

    Source documentation

    The connected edge-cancellation surgery preserves literal genus zero and removes exactly one face and two darts.

    theorem mergeEdge_genusZero (hG : M.GenusZero) : (M.mergeEdge h).GenusZero := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero