OAI/Geometry/HyperbolicGroups/ConeCellTarget.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.TopPolygon line 20
  2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Square line 21
  3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Six line 23
  4. def OAI.HyperbolicObstruction.ConeSkeleton.extendRow line 27

    Source documentation

    Only actual positions index rows; this extension is a device for reading an oriented word and cannot introduce duplicate row occurrences.

    def extendRow (r : Row) (l : rowSupport r → Alphabet n) : Field → Alphabet n :=
…
  5. lemma OAI.HyperbolicObstruction.ConeSkeleton.row_extend line 30
  6. def OAI.HyperbolicObstruction.ConeSkeleton.squareSide line 37
  7. lemma OAI.HyperbolicObstruction.ConeSkeleton.squareSide_start line 43
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.squareSide_end line 47
  9. def OAI.HyperbolicObstruction.ConeSkeleton.topSide line 51
  10. lemma OAI.HyperbolicObstruction.ConeSkeleton.topSide_closed line 54
  11. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Cell line 62

    Source documentation

    The three actual kinds of faces AFTER radial top triangles have been assembled and the closed macro walks split into simple cycles. Such assembly and its genus preservation are separate obligations, not fields here.

    abbrev Cell := FanTriangle n w ⊕ (TopPolygon n w ⊕ (Square n w ⊕ Six n d))

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.TopPolygon, OAI.HyperbolicObstruction.ConeSkeleton.Square, OAI.HyperbolicObstruction.ConeSkeleton.Six

  12. def OAI.HyperbolicObstruction.ConeSkeleton.size line 64
  13. def OAI.HyperbolicObstruction.ConeSkeleton.side line 70
  14. lemma OAI.HyperbolicObstruction.ConeSkeleton.size_positive line 76
  15. lemma OAI.HyperbolicObstruction.ConeSkeleton.size_le line 83
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.side_closed line 90
  17. def OAI.HyperbolicObstruction.ConeSkeleton.boundary line 98
  18. def OAI.HyperbolicObstruction.ConeSkeleton.target line 110

    Source documentation

    Fully specified indexed oriented boundaries for actual included rows. This is a concrete instantiation of normal-picture cancellation, not an abstract diagram carrying the desired fan bound or isoperimetry.

    def target {A : Type*} [AddCommGroup A] (weight : Cell n w d → A) :=
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Cell

  19. lemma OAI.HyperbolicObstruction.ConeSkeleton.slot_injective line 113
  20. lemma OAI.HyperbolicObstruction.ConeSkeleton.top_apex_injective line 120

    Source documentation

    A simple top polygon visits each actual fan occurrence at most once. Different point types remain different occurrences even if every letter in their rows has the same value.

    lemma top_apex_injective (a : TopPolygon n w) (i j : Fin a.2.2.val.length)
    (b : Fan n w) (hi : start n w (topSide n w a i) = .inr b)
    (hj : start n w (topSide n w a j) = .inr b) : i = j := by
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.TopPolygon, OAI.HyperbolicObstruction.ConeSkeleton.Fan, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.topSide