OAI/Geometry/HyperbolicGroups/FinitePolygonModel.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

A finite simplicial model of a literal finite polygon incidence system. All edges are split three times, and every boundary occurrence has its own collar vertex. Thus loops, repeated boundary vertices and parallel edges are not silently identified. The carrier/homotopy comparison is a later theorem.

  1. structure OAI.HyperbolicObstruction.FinitePolygonModel.Data line 15
  2. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.Position line 27
  3. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.GraphVertex line 28
  4. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.Vertex line 29
  5. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.graph line 31
  6. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.old line 32
  7. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.mid line 33
  8. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.apex line 34
  9. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.outer line 35
  10. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.next line 37
  11. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.next_ne line 41
  12. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.dartStart line 53

    Source documentation

    Start of one of the three subdivided segments of a signed old edge.

    def dartStart (e : E × Bool) (j : Fin 3) : P.Vertex :=
…
  13. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.base line 57
  14. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.graphFace line 62

    Source documentation

    The three positive graph segments.

    def graphFace (e : E) (j : Fin 3) : Finset P.Vertex :=
…
  15. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.collarFace line 68

    Source documentation

    Two simplices in each mapping-cylinder rectangle and one cap simplex.

    def collarFace (q : P.Position) (j : Fin 3) : Finset P.Vertex :=
…
  16. abbrev OAI.HyperbolicObstruction.FinitePolygonModel.Data.Facet line 73
  17. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.facet line 74
  18. def OAI.HyperbolicObstruction.FinitePolygonModel.Data.complex line 78
  19. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.facet_face line 88
  20. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.simplex_card_le_three line 94
  21. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.edge_of_facet line 104
  22. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.joined_of_facet line 113
  23. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.mid_joined_start line 117
  24. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.endpoints_joined line 123
  25. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.outer_joined_base line 130
  26. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.apex_joined_outer line 134
  27. lemma OAI.HyperbolicObstruction.FinitePolygonModel.Data.pathConnected_of_graph line 142

    Source documentation

    Connectedness is reduced exactly to the old graph, not assumed for the new carrier.

    lemma pathConnected_of_graph (v : V)
    (h : ∀ w : V, Joined (vertex P.complex (P.old v)) (vertex P.complex (P.old w))) :
    PathConnectedSpace (Carrier P.complex) := by
…