OAI/Geometry/HyperbolicGroups/ConeLetterCollapse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.ConeSkeleton.radialWord line 16
  2. def OAI.HyperbolicObstruction.ConeSkeleton.collapse line 22

    Source documentation

    Literal radial-path collapse of the actual cone one-skeleton. It fixes all letter edges, and does not identify two indexed radial positions.

    def collapse : Dart n w → List (Alphabet n)
  | (.inl a,b) => [(a,b)]
  | (.inr ⟨f,v⟩,true) => radialWord n w f v
  | (.inr ⟨f,v⟩,false) => FreeGroup.invRev (radialWord n w f v)

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.ConeSkeleton.radialWord

  3. lemma OAI.HyperbolicObstruction.ConeSkeleton.collapse_rev line 27
  4. lemma OAI.HyperbolicObstruction.ConeSkeleton.collapse_letter line 31
  5. lemma OAI.HyperbolicObstruction.ConeSkeleton.collapse_length line 33
  6. def OAI.HyperbolicObstruction.ConeSkeleton.collapsedBoundary line 42
  7. lemma OAI.HyperbolicObstruction.ConeSkeleton.fan_edge_adj line 45
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.fan_edge_label line 49
  9. def OAI.HyperbolicObstruction.ConeSkeleton.fanCollapsedWalk line 56
  10. lemma OAI.HyperbolicObstruction.ConeSkeleton.fanCollapsedWalk_length line 62
  11. lemma OAI.HyperbolicObstruction.ConeSkeleton.fanCollapsedWalk_word line 68
  12. theorem OAI.HyperbolicObstruction.ConeSkeleton.fan_collapse_filling line 79

    Source documentation

    The actual source fan-triangle substitution, including backtracking fan paths, needs no more than five faces of the finite simple-cycle presentation.

    theorem fan_collapse_filling (f : FanTriangle n w) :
    ∃ a ≤ 5, WordPictures.Homotopy (SimpleWordRelator n w d)
      (collapsedBoundary n w d (.inl f)) [] a := by
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.collapsedBoundary