OAI/GroupTheory/Hyperbolic/WordPaths.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

A combinatorial fundamental groupoid of the un-collapsed triangle complex. The quotient imposes only its triangular faces. Tree edges are used for basing, not mistaken for triangular two-cells in a van Kampen diagram.

  1. inductive OAI.Release075.BlockPresentation.Vertex line 14
  2. inductive OAI.Release075.BlockPresentation.Arrow line 17
  3. instance OAI.Release075.BlockPresentation.vertexQuiver line 22
  4. abbrev OAI.Release075.BlockPresentation.FreePaths line 24
  5. def OAI.Release075.BlockPresentation.freeVertex line 26
  6. def OAI.Release075.BlockPresentation.freeX line 28
  7. def OAI.Release075.BlockPresentation.freeL line 30
  8. def OAI.Release075.BlockPresentation.freeR line 32
  9. inductive OAI.Release075.BlockPresentation.FaceRelation line 35
  10. abbrev OAI.Release075.BlockPresentation.FundamentalGroupoid line 42
  11. def OAI.Release075.BlockPresentation.vertex line 44
  12. def OAI.Release075.BlockPresentation.pathX line 47
  13. def OAI.Release075.BlockPresentation.pathL line 49
  14. def OAI.Release075.BlockPresentation.pathR line 51
  15. theorem OAI.Release075.BlockPresentation.path_triangle line 54
  16. abbrev OAI.Release075.BlockPresentation.FundamentalGroup line 62

    Source documentation

    Path-order multiplication is the opposite of Mathlib's End multiplication.

    abbrev FundamentalGroup := (End (d.vertex .o))ᵐᵒᵖ
  17. def OAI.Release075.BlockPresentation.treePathV line 64
  18. def OAI.Release075.BlockPresentation.treePathW line 65
  19. def OAI.Release075.BlockPresentation.basedEdge line 67
  20. theorem OAI.Release075.BlockPresentation.based_triangle line 72
  21. theorem OAI.Release075.BlockPresentation.based_treeL line 83
  22. theorem OAI.Release075.BlockPresentation.based_treeR line 88
  23. def OAI.Release075.BlockPresentation.toFundamentalGroup line 93
  24. theorem OAI.Release075.BlockPresentation.toFundamentalGroup_edge line 100
  25. def OAI.Release075.BlockPresentation.edgeEvaluation line 104

    Source documentation

    Evaluation in the displayed group presentation, before quotienting faces.

    def edgeEvaluation : d.Vertex ⥤q SingleObj d.GroupTypeᵐᵒᵖ where
…
  26. def OAI.Release075.BlockPresentation.freeEvaluation line 111
  27. theorem OAI.Release075.BlockPresentation.freeEvaluation_generator line 114
  28. def OAI.Release075.BlockPresentation.evaluation line 119
  29. theorem OAI.Release075.BlockPresentation.evaluation_pathX line 129
  30. theorem OAI.Release075.BlockPresentation.evaluation_pathL line 134
  31. theorem OAI.Release075.BlockPresentation.evaluation_pathR line 139
  32. def OAI.Release075.BlockPresentation.fromFundamentalGroup line 144
  33. theorem OAI.Release075.BlockPresentation.fromFundamentalGroup_basedEdge line 155
  34. theorem OAI.Release075.BlockPresentation.from_to_fundamental line 174
  35. theorem OAI.Release075.BlockPresentation.toFundamentalGroup_injective line 181
  36. abbrev OAI.Release075.BlockPresentation.RawPaths line 191
  37. def OAI.Release075.BlockPresentation.rawVertex line 193
  38. def OAI.Release075.BlockPresentation.rawX line 195
  39. def OAI.Release075.BlockPresentation.rawL line 197
  40. def OAI.Release075.BlockPresentation.rawR line 199
  41. inductive OAI.Release075.BlockPresentation.RawMove line 202
  42. def OAI.Release075.BlockPresentation.RawHomotopic line 211
  43. abbrev OAI.Release075.BlockPresentation.RawQuotient line 214
  44. def OAI.Release075.BlockPresentation.freeToRawQuotient line 216
  45. def OAI.Release075.BlockPresentation.fundamentalToRawQuotient line 222
  46. def OAI.Release075.BlockPresentation.rawToFundamental line 231
  47. theorem OAI.Release075.BlockPresentation.rawMove_sound line 235
  48. def OAI.Release075.BlockPresentation.rawQuotientToFundamental line 244
  49. theorem OAI.Release075.BlockPresentation.raw_equality_iff line 249

    Source documentation

    Equality in the two-stage groupoid quotient is exactly a finite chain of triangle moves and backtrack moves in arbitrary typed path contexts.

    theorem raw_equality_iff {a c : d.RawPaths} (p q : a ⟶ c) :
    d.rawToFundamental.map p = d.rawToFundamental.map q ↔ d.RawHomotopic p q := by
…
  50. def OAI.Release075.BlockPresentation.rawRectangle line 262
  51. theorem OAI.Release075.BlockPresentation.rawToFundamental_X line 266
  52. theorem OAI.Release075.BlockPresentation.rawToFundamental_reverse line 269
  53. theorem OAI.Release075.BlockPresentation.based_rectangle_formula line 273
  54. theorem OAI.Release075.BlockPresentation.rawRectangle_nullhomotopic_of_eq_one line 287

    Source documentation

    If a rectangular word vanished in the actual presentation, the unbased four-edge rectangle would have a finite triangle/backtrack nullhomotopy.

    theorem rawRectangle_nullhomotopic_of_eq_one (i : I) (u u' v v' : Fin r)
    (h : d.x i u v * (d.x i u' v)⁻¹ * d.x i u' v' * (d.x i u v')⁻¹ = 1) :
    d.RawHomotopic (d.rawRectangle i u u' v v') (𝟙 _) := by
…