OAI/Geometry/HyperbolicGroups/GraphGroupWalk.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.GraphGroupWalk.eval line 14
2. lemma OAI.HyperbolicObstruction.GraphGroupWalk.eval_nil line 15
3. lemma OAI.HyperbolicObstruction.GraphGroupWalk.eval_cons line 16
4. lemma OAI.HyperbolicObstruction.GraphGroupWalk.eval_append line 18
5. lemma OAI.HyperbolicObstruction.GraphGroupWalk.short_loop_eval line 21
6. theorem OAI.HyperbolicObstruction.GraphGroupWalk.reduce_to_path line 36

   Source documentation

   Noncommutative loop erasure. Killing all elementary cycles suffices; commutativity, a commutator relation, or graph connectedness is not assumed.

   theorem reduce_to_path (c : G.Dart → H) (hc : ∀ d, c d.symm = (c d)⁻¹)
       (hcycle : ∀ (u : V) (p : G.Walk u u), p.IsCycle → eval c p = 1)
       {u v : V} (p : G.Walk u v) :
       ∃ q : G.Walk u v, q.IsPath ∧ eval c p = eval c q := by
   …

   Mentions: OAI.HyperbolicObstruction.GraphGroupWalk.eval

7. theorem OAI.HyperbolicObstruction.GraphGroupWalk.closed_eval_one line 64
8. lemma OAI.HyperbolicObstruction.GraphGroupWalk.eval_reverse line 72
9. theorem OAI.HyperbolicObstruction.GraphGroupWalk.route_edge line 83

   Source documentation

   Route potentials under elementary-cycle relations. Only the chosen routes, not a spanning-tree axiom, are needed.

   theorem route_edge (c : G.Dart → H) (hc : ∀ d, c d.symm = (c d)⁻¹)
       (hcycle : ∀ (u : V) (p : G.Walk u u), p.IsCycle → eval c p = 1)
       {r u v : V} (p : G.Walk r u) (q : G.Walk r v) (h : G.Adj u v) :
       eval c p * c ⟨(u,v),h⟩ = eval c q := by
   …

   Mentions: OAI.HyperbolicObstruction.GraphGroupWalk.eval