OAI/Geometry/HyperbolicGroups/ConePresentationGroup.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.PolygonGroup line 19

   Source documentation

   The actual indexed polygon words. Radial edges are not silently equated or turned into extra letter relators. This bouquet presentation has extra free factors relative to the graph fundamental group, but the original letter relations still hold in it, which is all the disk producer needs.

   abbrev PolygonGroup := PresentedGroup (FreeGroup.mk '' Set.range (boundary n w d).attachingWord)

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.boundary

2. def OAI.HyperbolicObstruction.ConeSkeleton.polygonValue line 21
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.polygonValue_rev line 23
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.polygonValue_word line 29
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.polygonValue_cell line 39
6. def OAI.HyperbolicObstruction.ConeSkeleton.freeComparison line 47
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.freeComparison_letter line 50
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.freeComparison_word line 56
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.freeComparison_relator line 66

   Source documentation

   Both arbitrary closed-walk relator families, including the exceptional loose edge, and both decoration families are consequences of the literal fan triangles and simple macro polygons.

   lemma freeComparison_relator (r : FreeGroup (Fin (n+1))) (hr : Relator n w d r) :
       freeComparison n w d r = 1 := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.freeComparison

10. lemma OAI.HyperbolicObstruction.ConeSkeleton.relator_normalClosure_le line 88
11. theorem OAI.HyperbolicObstruction.ConeSkeleton.nullWord_to_polygon line 96

    Source documentation

    No round trip or presentation-equivalence assumption: every original null letter word is an actual cone-polygon nullword.

    theorem nullWord_to_polygon (z : List (Alphabet n))
        (hz : PresentedGroup.mk (Relator n w d) (FreeGroup.mk z) = 1) :
        PresentedGroup.mk (FreeGroup.mk '' Set.range (boundary n w d).attachingWord)
          (FreeGroup.mk (z.map (letterDart n w))) = 1 := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.letterDart