OAI/Geometry/HyperbolicGroups/PresentationDisk.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.LetterPresentation.freeLetter_mk line 17
2. lemma OAI.HyperbolicObstruction.LetterPresentation.mk_prod line 21
3. def OAI.HyperbolicObstruction.LetterPresentation.stepLetter line 29
4. lemma OAI.HyperbolicObstruction.LetterPresentation.mk_stepLetter line 32
5. def OAI.HyperbolicObstruction.LetterPresentation.pathWord line 37
6. lemma OAI.HyperbolicObstruction.LetterPresentation.pathWord_length line 41
7. lemma OAI.HyperbolicObstruction.LetterPresentation.mk_pathWord line 47
8. def OAI.HyperbolicObstruction.LetterPresentation.literalSquare line 56
9. lemma OAI.HyperbolicObstruction.LetterPresentation.mk_literalSquare line 59
10. inductive OAI.HyperbolicObstruction.LetterPresentation.WordRelator line 72

    Source documentation

    Literal boundaries, retaining every side index of its graph walk or row. The arbitrary fan/top walks will later be reduced to a finite list of defining cycles; the disk theorem here has no area estimate.

    inductive WordRelator : List (Alphabet n) → Prop
      | fan (l : Field → Alphabet n) (i : Fin 7)
          (present : w (TableModel.row rowSupport l (.inl i)) = true)
          (v : MasterGraph.Vertex) (p : MasterGraph.Path v v)
          (fields : p.fields.toFinset ⊆ rowSupport (.inl i)) : WordRelator (pathWord n l p)
      | top (l : Field → Alphabet n)
          (present : w (TableModel.row rowSupport l (.inr (.inl ()))) = true)
          (fans : ∀ i : Fin 7, w (TableModel.row rowSupport l (.inl i)) = true)
          (v : MasterGraph.Vertex) (p : MasterGraph.Path v v) (core : p.IsCore) :
          WordRelator (pathWord n l p)
      | square (l : Field → Alphabet n) (τ : TwoPath)
          (present : w (TableModel.row rowSupport l (.inr (.inr τ))) = true) :
    …

    Mentions: OAI.HyperbolicObstruction.LetterPresentation.Alphabet, OAI.HyperbolicObstruction.TableModel.row, OAI.HyperbolicObstruction.MasterGraph.Vertex, OAI.HyperbolicObstruction.MasterGraph.Path, OAI.HyperbolicObstruction.LetterPresentation.pathWord

11. lemma OAI.HyperbolicObstruction.LetterPresentation.mk_ofFn line 87
12. lemma OAI.HyperbolicObstruction.LetterPresentation.wordRelator_image line 91
13. theorem OAI.HyperbolicObstruction.LetterPresentation.null_word_disk line 121

    Source documentation

    Every null literal letter word has a finite disk derivation over the actual included fan/top/decorations, with free cancellations accounted for at zero cost. This is the algebraic part of source diagram:existence.

    theorem null_word_disk (z : List (Alphabet n))
        (hz : PresentedGroup.mk (Relator n w d) (FreeGroup.mk z) = 1) :
        ∃ a, WordPictures.Homotopy (WordRelator n w d) z [] a := by
    …

    Mentions: OAI.HyperbolicObstruction.LetterPresentation.Alphabet, OAI.HyperbolicObstruction.LetterPresentation.Relator, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.LetterPresentation.WordRelator