OAI/Geometry/HyperbolicGroups/WordPictureExist.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.rotate line 17
  2. def OAI.HyperbolicObstruction.WordPictures.WordPicture.rotate line 32
  3. def OAI.HyperbolicObstruction.WordPictures.WordPicture.conjugateLetter line 43
  4. def OAI.HyperbolicObstruction.WordPictures.WordPicture.conjugate line 53
  5. def OAI.HyperbolicObstruction.WordPictures.pictureSubgroup line 64

    Source documentation

    Elements represented by actual finite genus-zero diagrams. The subgroup and its normality are proved by gluing, reflecting and attaching a whisker.

    def pictureSubgroup (R : Set (Word A)) : Subgroup (FreeGroup A) where
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.Word

  6. instance OAI.HyperbolicObstruction.WordPictures.(instance at line 74) line 74
  7. theorem OAI.HyperbolicObstruction.WordPictures.picture_existence line 83

    Source documentation

    Van Kampen realization at the freely represented boundary level: every null element has an actual finite genus-zero side-pairing with only the specified relator faces. The next literal-boundary step is free folding.

    theorem picture_existence {R : Set (Word A)} (w : Word A)
    (h : PresentedGroup.mk (FreeGroup.mk '' R) (FreeGroup.mk w) = 1) :
    ∃ v, FreeGroup.mk v = FreeGroup.mk w ∧ Nonempty (WordPicture R v) := by
…

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