OAI/Geometry/HyperbolicGroups/Graph.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.MasterGraph.Vertex line 14
  2. def OAI.HyperbolicObstruction.MasterGraph.left line 16
  3. def OAI.HyperbolicObstruction.MasterGraph.middle line 18
  4. def OAI.HyperbolicObstruction.MasterGraph.right line 20
  5. def OAI.HyperbolicObstruction.MasterGraph.source line 23
  6. def OAI.HyperbolicObstruction.MasterGraph.target line 27
  7. structure OAI.HyperbolicObstruction.MasterGraph.Step line 32

    Source documentation

    An oriented traversal of one of the fixed master fields.

    structure Step (a b : Vertex) where
…

    Mentions: OAI.HyperbolicObstruction.MasterGraph.Vertex

  8. def OAI.HyperbolicObstruction.MasterGraph.Step.pos line 40
  9. def OAI.HyperbolicObstruction.MasterGraph.Step.neg line 41
  10. def OAI.HyperbolicObstruction.MasterGraph.Step.symm line 42
  11. lemma OAI.HyperbolicObstruction.MasterGraph.Step.endpoints_pos line 49
  12. lemma OAI.HyperbolicObstruction.MasterGraph.Step.endpoints_neg line 51
  13. inductive OAI.HyperbolicObstruction.MasterGraph.Path line 56

    Source documentation

    Finite paths, with edges carrying their actual named fields.

    inductive Path : Vertex → Vertex → Type
  | nil (a : Vertex) : Path a a
  | cons {a b c : Vertex} (s : Step a b) (p : Path b c) : Path a c

namespace Path
variable {a b c : Vertex}

    Mentions: OAI.HyperbolicObstruction.MasterGraph.Vertex, OAI.HyperbolicObstruction.MasterGraph.Step

  14. def OAI.HyperbolicObstruction.MasterGraph.Path.length line 62
  15. def OAI.HyperbolicObstruction.MasterGraph.Path.fields line 66
  16. lemma OAI.HyperbolicObstruction.MasterGraph.Path.fields_length line 70
  17. def OAI.HyperbolicObstruction.MasterGraph.Path.append line 75
  18. def OAI.HyperbolicObstruction.MasterGraph.Path.symm line 79
  19. def OAI.HyperbolicObstruction.MasterGraph.coreStep line 85

    Source documentation

    Core adjacency corresponds to the unique actual core field.

    def coreStep {a b : CoreGeometry.Vertex} (h : CoreGeometry.Adjacent a b) : Step (.inl a) (.inl b) := by
…

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex, OAI.HyperbolicObstruction.CoreGeometry.Adjacent, OAI.HyperbolicObstruction.MasterGraph.Step

  20. def OAI.HyperbolicObstruction.MasterGraph.coreEdge line 97

    Source documentation

    The unoriented field of a core adjacency.

    def coreEdge {a b : CoreGeometry.Vertex} (h : CoreGeometry.Adjacent a b) : Edge := by
…

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.Vertex, OAI.HyperbolicObstruction.CoreGeometry.Adjacent

  21. lemma OAI.HyperbolicObstruction.MasterGraph.coreStep_field line 108
  22. lemma OAI.HyperbolicObstruction.MasterGraph.core_adj_ne line 112
  23. lemma OAI.HyperbolicObstruction.MasterGraph.coreEdge_eq line 115
  24. lemma OAI.HyperbolicObstruction.MasterGraph.coreEdge_fan line 123
  25. lemma OAI.HyperbolicObstruction.MasterGraph.coreEdge_ne_consecutive line 128
  26. lemma OAI.HyperbolicObstruction.MasterGraph.coreEdge_ne_third line 135
  27. lemma OAI.HyperbolicObstruction.MasterGraph.corePath_three_nodup line 143
  28. def OAI.HyperbolicObstruction.MasterGraph.first line 153

    Source documentation

    The actual two core sides of a decoration.

    def first (τ : TwoPath) : Step (.inl (left τ)) (.inl (middle τ)) :=
…

    Mentions: OAI.HyperbolicObstruction.MasterGraph.Step, OAI.HyperbolicObstruction.MasterGraph.left, OAI.HyperbolicObstruction.MasterGraph.middle

  29. def OAI.HyperbolicObstruction.MasterGraph.second line 158
  30. lemma OAI.HyperbolicObstruction.MasterGraph.first_field line 165
  31. lemma OAI.HyperbolicObstruction.MasterGraph.second_field line 166
  32. def OAI.HyperbolicObstruction.MasterGraph.root line 169

    Source documentation

    A fixed anchor and genuine paths in the finite literal core graph.

    def root : Vertex := .inl (.inl 0)

    Mentions: OAI.HyperbolicObstruction.MasterGraph.Vertex

  33. theorem OAI.HyperbolicObstruction.MasterGraph.corePath_nonempty line 171
  34. def OAI.HyperbolicObstruction.MasterGraph.corePath line 195
  35. def OAI.HyperbolicObstruction.MasterGraph.route line 197
  36. lemma OAI.HyperbolicObstruction.MasterGraph.admissible_down line 202
  37. lemma OAI.HyperbolicObstruction.MasterGraph.admissible_core_triple line 215
  38. lemma OAI.HyperbolicObstruction.MasterGraph.corePath_three_admissible line 252