OAI/Geometry/HyperbolicGroups/PolygonSphereFurther.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.turn line 18
  2. def OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.flip line 24
  3. def OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.pairing line 32

    Source documentation

    The sphere obtained by pairing a polygon with a reversed copy. It is the literal base case of a cellular disk picture after adjoining its outside.

    def pairing : PictureMap (Bool × I) where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.turn_orientation line 38
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.face_sameCycle_pos line 40
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.face_sameCycle_neg line 44
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.face_classes line 48
  8. def OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.vertexIndex line 63

    Source documentation

    Vertex classifier for the doubled boundary: vertices are NOT assumed as incidence fields; they are computed from face-turn times side-pairing.

    def vertexIndex (x : Bool × I) : I := if x.1 then x.2 else q x.2
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.vertex_index line 65
  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.vertex_classes line 68
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.connected line 93
  12. theorem OAI.HyperbolicObstruction.PictureSwitch.PolygonSphere.genusZero line 108