OAI/Geometry/HyperbolicGroups/PictureUnderlyingGraph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GraphVertex line 22

   Source documentation

   The vertices of the actual rotation system, without collapsing darts or parallel edge copies. Only the associated simple adjacency ignores loops.

   abbrev GraphVertex := Quotient (SameCycle.setoid M.vertex)

2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexClass line 24
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexClass_eq_iff line 27
4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.underlyingGraph line 33

   Source documentation

   The underlying simple graph used in the planar-separator argument. Its adjacency is induced by real edge copies of the rotation system.

   def underlyingGraph : SimpleGraph M.GraphVertex where
   …

5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.underlying_adj_iff line 41
6. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.underlying_neighbor_card_le line 48

   Source documentation

   Distinct neighbors inject into actual incident darts. This is the exact reason the multigraph valence bound also bounds the underlying simple degree.

   theorem underlying_neighbor_card_le (v : M.GraphVertex) :
       Nat.card (M.underlyingGraph.neighborSet v) ≤ Nat.card {x : D // M.vertexClass x = v} := by
   …

7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex_fiber_equiv line 59
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.underlying_neighbor_card_le_cycle line 63
9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.components_le_underlying_reachable line 71
10. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphComponent line 85

    Source documentation

    Sending each rotation vertex to its true connected component.

    def graphComponent : M.GraphVertex → Quotient M.components :=
    …

11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphComponent_adj line 89
12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graphComponent_reachable line 95
13. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.underlying_reachable_iff line 105

    Source documentation

    Simple-graph reachability is exactly connectivity of the actual side identifications, not an additional assumption about a planar drawing.

    theorem underlying_reachable_iff (x y : D) :
        M.underlyingGraph.Reachable (M.vertexClass x) (M.vertexClass y) ↔ M.components x y := by
    …