OAI/Geometry/HyperbolicGroups/PictureTriangulation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.StarDart line 21

    Source documentation

    Three individually indexed sides for each old side: its old edge, and two radii to the new center of the old face. This is literal face starring.

    abbrev StarDart (D : Type*) := D ⊕ (D ⊕ D)
  2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starFace line 23
  3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starEdgeFun line 35
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starEdge_sq line 40
  5. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starEdge line 44
  6. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation line 52

    Source documentation

    A triangular rotation system obtained by starring every face; old edge copies are preserved, and each old face has a distinct new center.

    def triangulation : PictureMap (StarDart D) where
…

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

  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_left line 62
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_middle line 64
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_right line 66
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_vertex_left line 68
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_vertex_middle line 70
  12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_vertex_right line 72
  13. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.starIndex line 75
  14. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.star_face_to_left line 77
  15. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_cycle line 84
  16. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_cycles line 96
  17. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.triangulation_face_degree line 103

    Source documentation

    All new faces have exactly three sides, including when the old map had loops, multiple edges, or monogons.

    lemma triangulation_face_degree (x : StarDart D) :
    Fintype.card {y : StarDart D // M.triangulation.face.SameCycle x y} = 3 := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.StarDart