OAI/Geometry/HyperbolicGroups/BoundaryFold.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryPinch line 21

    Source documentation

    Pinch the two consecutive boundary sides off as a genuine bigon. The other side pairs are unchanged, and the remaining boundary bypasses them.

    def boundaryPinch (_ : a ≠ b) (_ : M.face a = b) : PictureMap D := M.splice b (M.face⁻¹ a)
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryPinch_bigon line 24
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryPinch_genusZero line 36
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryPinch_respects line 53
  5. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold line 70

    Source documentation

    Literal free boundary cancellation, valid even when either canceled side was paired to an interior side or to another part of the outside. It is a genus-zero operation, not an assumed disk replacement.

    def boundaryFold : PictureMap {x // OffPair a b x} :=
…

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

  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_genusZero line 73
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_respects line 77
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_face line 83
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_face_orbits line 101
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryFold_other_face line 112

    Source documentation

    No cell-side index on another face changes. This is the compatibility needed to turn algebraic free reduction into an actual mapped disk picture.

    lemma boundaryFold_other_face (x : {x // OffPair a b x})
    (hx : ¬ M.face.SameCycle a x.val) :
    ((M.boundaryFold hab hnext).face x).val = M.face x.val := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.OffPair