OAI/Geometry/HyperbolicGroups/PictureCotreeColor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertexClass_vertex line 22
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.dual_vertexClass_face line 26
  3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.faceCorners line 32

    Source documentation

    The actual corners of a selected dual vertex (primal face).

    def faceCorners (f : M.dual.GraphVertex) : Finset M.GraphVertex :=
…
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.corner_mem line 36
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.corner_opposite_mem line 41
  6. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotreeGraph line 49
  7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotreeColor line 54

    Source documentation

    Colors are ACTUAL components of the complementary dual graph after isolating one specified face; the face itself receives its isolated color.

    def cotreeColor (f : M.dual.GraphVertex) (x : D) :
    ((M.cotreeGraph q hq).deleteIncidenceSet f).ConnectedComponent :=
…
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotreeColor_face line 59
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotreeColor_fixed_edge line 65
  10. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.cotree_color_boundary_in_path_hull line 85

    Source documentation

    The rooted paths to the corners of a dual-tree vertex contain every edge across which the associated deleted-dual-component color changes. Unlike an abstract Jordan-curve assumption, this follows from the exact rotation permutations, genus-zero Euler formula and tree copy counts.

    theorem cotree_color_boundary_in_path_hull (hG : M.GenusZero)
    (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
    (hboundary : cycles (M.vertex*q) = 1) (root : M.GraphVertex)
    (f : M.dual.GraphVertex) :
    ∀ x, M.cotreeColor q hq f (M.edge x) ≠ M.cotreeColor q hq f x →
      M.vertexClass x ∈ treePathHull (M.subpairingGraph q (M.subpairing_sq q hq))
        (M.subpairing_isTree hG q hq hspan hboundary) root (M.faceCorners f) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles