OAI/Geometry/HyperbolicGroups/Presentation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.MasterGraph.Path.IsCore line 19
  2. lemma OAI.HyperbolicObstruction.MasterGraph.Path.isCore_append line 20
  3. lemma OAI.HyperbolicObstruction.MasterGraph.Path.isCore_symm line 29
  4. lemma OAI.HyperbolicObstruction.MasterGraph.Path.eval_map line 38
  5. theorem OAI.HyperbolicObstruction.MasterGraph.coreRoute_exists line 49
  6. def OAI.HyperbolicObstruction.MasterGraph.coreRoute line 72
  7. lemma OAI.HyperbolicObstruction.MasterGraph.coreRoute_core line 73
  8. def OAI.HyperbolicObstruction.MasterGraph.squareWord line 77

    Source documentation

    The oriented source four-letter decoration, including the two given core sides.

    def squareWord {G L : Type*} [Group G] (l : Field → L) (r : L → G) (τ : TwoPath) : G :=
…
  9. lemma OAI.HyperbolicObstruction.MasterGraph.squareWord_map line 80
  10. abbrev OAI.HyperbolicObstruction.LetterPresentation.Alphabet line 91
  11. def OAI.HyperbolicObstruction.LetterPresentation.freeLetter line 93
  12. def OAI.HyperbolicObstruction.LetterPresentation.inverseLetter line 96
  13. lemma OAI.HyperbolicObstruction.LetterPresentation.freeLetter_inv line 102
  14. inductive OAI.HyperbolicObstruction.LetterPresentation.Relator line 112

    Source documentation

    The literal source letter relators: all included fans, all included top occurrences (with all seven fan slots), and every included square/six-letter row, even rows that do not occur in any master match.

    inductive Relator : FreeGroup (Fin (n+1)) → 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)) : Relator (p.eval l (freeLetter n))
  | 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) :
      Relator (p.eval l (freeLetter n))
  | 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.freeLetter

  15. abbrev OAI.HyperbolicObstruction.LetterPresentation.Group line 128
  16. instance OAI.HyperbolicObstruction.LetterPresentation.group line 129
  17. def OAI.HyperbolicObstruction.LetterPresentation.letter line 131
  18. lemma OAI.HyperbolicObstruction.LetterPresentation.letter_inv line 133
  19. lemma OAI.HyperbolicObstruction.LetterPresentation.letter_generates line 136
  20. lemma OAI.HyperbolicObstruction.LetterPresentation.top_relator line 143
  21. lemma OAI.HyperbolicObstruction.LetterPresentation.square_relator line 149
  22. lemma OAI.HyperbolicObstruction.LetterPresentation.six_relator line 155
  23. def OAI.HyperbolicObstruction.LetterPresentation.coreValue line 161
  24. lemma OAI.HyperbolicObstruction.LetterPresentation.coreValue_path line 164
  25. def OAI.HyperbolicObstruction.LetterPresentation.vertexValue line 174
  26. lemma OAI.HyperbolicObstruction.LetterPresentation.coreValue_step line 178
  27. def OAI.HyperbolicObstruction.LetterPresentation.potential line 190

    Source documentation

    Every master match has a genuine group-valued potential in the literal letter presentation. Only its actual top and square relators are used.

    def potential (a : StarModel.Matches rowSupport w) : Potential a.val (letter n w d) where
…

    Mentions: OAI.HyperbolicObstruction.StarModel.Matches, OAI.HyperbolicObstruction.LetterPresentation.letter

  28. lemma OAI.HyperbolicObstruction.LetterPresentation.six_tail_relator line 212