OAI/Geometry/HyperbolicGroups/PictureMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PictureSwitch.PictureMap line 19

    Source documentation

    Oriented polygonal side-pairings (darts are individually indexed sides). face turns around each polygon; edge pairs sides with opposite orientation. Vertices are the cycles of face * edge, so no abstract vertex incidences or Euler changes are supplied as hypotheses.

    structure PictureMap (D : Type*) where
…
  2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex line 28
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.edge_edge line 30
  4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch line 38

    Source documentation

    Crosswise re-pairing of the two specified outgoing sides. All original face cycles (hence all original corners and their maps) are unchanged.

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

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_face line 53
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex_switch line 55
  7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler line 67
  8. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_vertices line 71

    Source documentation

    Exact vertex count under the radial switch in the manuscript. The two far vertices are either joined, or each original link is split.

    theorem switch_vertices (a b : D) (hab : a ≠ b)
    (hv : M.vertex.SameCycle a b)
    (hfar₁ : ¬ M.vertex.SameCycle a (M.edge a))
    (hfar₂ : ¬ M.vertex.SameCycle a (M.edge b)) :
    cycles (M.switch a b).vertex = cycles M.vertex +
      if M.vertex.SameCycle (M.edge a) (M.edge b) then 2 else 0 := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex

  9. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_euler line 90

    Source documentation

    No appeal to a drawing is used for the Euler change; all faces and edges are retained, while the exact vertex-cycle computation gives the change.

    theorem switch_euler (a b : D) (hab : a ≠ b)
    (hv : M.vertex.SameCycle a b)
    (hfar₁ : ¬ M.vertex.SameCycle a (M.edge a))
    (hfar₂ : ¬ M.vertex.SameCycle a (M.edge b)) :
    (M.switch a b).euler = M.euler +
      if M.vertex.SameCycle (M.edge a) (M.edge b) then 2 else 0 := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.euler