OAI/Geometry/HyperbolicGroups/FanRoute.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.CoreWordGraph.base line 15
2. def OAI.HyperbolicObstruction.CoreWordGraph.common line 16
3. lemma OAI.HyperbolicObstruction.CoreWordGraph.base_to_port line 18
4. lemma OAI.HyperbolicObstruction.CoreWordGraph.common_port line 24
5. lemma OAI.HyperbolicObstruction.CoreWordGraph.common_to_rep line 28
6. def OAI.HyperbolicObstruction.CoreWordGraph.fanRoute line 36

   Source documentation

   The source's fixed fan paths, length at most two, in the actual indexed fan before its edge labels are identified in the bouquet.

   def fanRoute (i : Fin 7) (v : FanVertex i) : (graph (fan i)).Walk (.inl (base i)) v.val := by
   …

   Mentions: OAI.HyperbolicObstruction.CoreWordGraph.graph, OAI.HyperbolicObstruction.CoreWordGraph.base

7. lemma OAI.HyperbolicObstruction.CoreWordGraph.fanRoute_length line 41
8. def OAI.HyperbolicObstruction.CoreWordGraph.inclusion line 46

   Source documentation

   Inclusion in the core does not alter the orientation or the literal random field used by an edge.

   def inclusion (S : Finset IncidenceTemplate.Edge) : graph S →g graph Finset.univ where
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Edge, OAI.HyperbolicObstruction.CoreWordGraph.graph

9. lemma OAI.HyperbolicObstruction.CoreWordGraph.inclusion_label line 53
10. lemma OAI.HyperbolicObstruction.CoreWordGraph.inclusion_word line 60