OAI/Geometry/HyperbolicGroups/WordPictureLiteral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.WordPictures.WordPicture.insertAt line 20

   Source documentation

   Inserting a freely canceling pair is attaching a thickened edge at the specified exterior corner, including the formerly empty exterior.

   def insertAt (P : WordPicture R w) {l r : Word A} (he : w = l++r) (a : A × Bool) :
       WordPicture R (l++a::invLetter a::r) := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.WordPicture, OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.invLetter

2. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_reverse_step line 31
3. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_reverse_red line 36
4. lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_free_eq line 42
5. theorem OAI.HyperbolicObstruction.WordPictures.literal_picture_existence line 53

   Source documentation

   Literal van Kampen disk realization from the ordinary presented group. All sides and relator boundaries are indexed; the map is genuinely finite and genus zero. There is no disk realization, area bound, or planarity premise. This producer handles arbitrary (not just reduced or nonempty) null words.

   theorem literal_picture_existence {R : Set (Word A)} (w : Word A)
       (h : PresentedGroup.mk (FreeGroup.mk '' R) (FreeGroup.mk w) = 1) :
       Nonempty (WordPicture R w) := by
   …

   Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture