OAI/Geometry/HyperbolicGroups/PolygonTarget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary line 21

    Source documentation

    An actual finite closed edge boundary for each cell, with indexed sides. The cell type may be infinite (as in the universal cover); every cell boundary is finite. Orientation reversal is constructed, not postulated.

    structure Boundary (C : Type*) (L : Type*) (V : Type*) where
…
  2. abbrev OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.Side line 32
  3. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.next line 34
  4. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.opposite line 40
  5. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.sideLabel line 46
  6. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.weight line 48
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.opposite_sq line 50
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.reverse_next line 54
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.orientation_next line 57
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.orientation_cycle line 59
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.opposite_cycle line 62
  12. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.edge_opposite line 67
  13. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.next_start line 70
  14. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.weight_next line 78
  15. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.weight_opposite line 80
  16. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.target line 85

    Source documentation

    The exact indexed oriented cell target constructed from ordinary polygon boundaries, suitable for CellPicture.normalize.

    def target (w : C → A) (apex : V → Bool)
    (hr : ∀ l, apex (B.start l) = true → apex (B.start (B.rev l)) = false) :
    CellTarget B.Side L V A where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.CellTarget

  17. theorem OAI.HyperbolicObstruction.PictureSwitch.CellTarget.respects_of_edge line 114

    Source documentation

    For genuine closed target cell boundaries, vertex-map compatibility follows from indexed face maps and the literal opposite-edge labels.

    theorem respects_of_edge (M : PictureMap D) (j : D → S)
    (hj : IndexedFaceMap M.face T.next j)
    (he : ∀ x, T.edge (j (M.edge x)) = T.rev (T.edge (j x))) :
    M.Respects (T.edge ∘ j) T.start T.rev := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap