OAI/Geometry/HyperbolicGroups/WordDisk.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Algebraic van Kampen existence, with actual words and area-counted local moves (not a finiteness or isoperimetric assumption). Free cancellation has zero cost; each orientation of a listed relator disk has cost one.

  1. abbrev OAI.HyperbolicObstruction.WordPictures.Word line 16
  2. inductive OAI.HyperbolicObstruction.WordPictures.Move line 18
  3. inductive OAI.HyperbolicObstruction.WordPictures.Homotopy line 24
  4. lemma OAI.HyperbolicObstruction.WordPictures.Move.contextual line 32
  5. lemma OAI.HyperbolicObstruction.WordPictures.Move.reverse line 40
  6. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.contextual line 53
  7. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.reverse line 60
  8. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.of_reduction line 68
  9. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.free line 74

    Source documentation

    Equality in the free group uses only free folds, not a face relator.

    lemma free (h : FreeGroup.mk u = FreeGroup.mk v) : Homotopy R u v 0 := by
…

    Mentions: OAI.HyperbolicObstruction.WordPictures.Homotopy

  10. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.append line 78
  11. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.append_null line 86
  12. lemma OAI.HyperbolicObstruction.WordPictures.Homotopy.conjugate line 89
  13. def OAI.HyperbolicObstruction.WordPictures.nullSubgroup line 99

    Source documentation

    Freely represented words admitting a finite disk construction.

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

    Mentions: OAI.HyperbolicObstruction.WordPictures.Word

  14. instance OAI.HyperbolicObstruction.WordPictures.(instance at line 109) line 109
  15. lemma OAI.HyperbolicObstruction.WordPictures.relators_in_null line 115
  16. theorem OAI.HyperbolicObstruction.WordPictures.existence line 121

    Source documentation

    Null words in the ordinary presented group have a finite area-counted word disk. No boundedness, reducedness or planarity premise is required.

    theorem existence {R : Set (Word A)} (w : Word A)
    (h : PresentedGroup.mk (FreeGroup.mk '' R) (FreeGroup.mk w) = 1) :
    ∃ n, Homotopy R w [] n := by
…

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

  17. lemma OAI.HyperbolicObstruction.WordPictures.move_sound line 129
  18. lemma OAI.HyperbolicObstruction.WordPictures.sound line 144