OAI/Geometry/HyperbolicGroups/FaceSplice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice line 22

    Source documentation

    Splicing oriented boundary polygons at their outgoing corners. This is connected sum at the outside faces when the two corners are in distinct components; no edge or side map is changed.

    def splice (a b : D) : PictureMap D where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_vertex line 29
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_components_le line 36
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_le_splice line 48
  5. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_components line 64

    Source documentation

    Two components are joined, with their actual new component equivalence exactly the quotient gluing relation.

    theorem splice_components (a b : D) (h : ¬ M.components a b) :
    (M.splice a b).components = glue M.components a b := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components, OAI.HyperbolicObstruction.PictureSwitch.glue

  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_euler line 72
  7. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.splice_genusZero line 88

    Source documentation

    Joining two genus-zero components along the outside face preserves genus zero. This is the finite combinatorial gluing used to assemble disk pictures.

    theorem splice_genusZero (hM : M.GenusZero) (a b : D) (h : ¬ M.components a b) :
    (M.splice a b).GenusZero := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GenusZero