OAI/Geometry/HyperbolicGroups/SquareBoundaryExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Four actual edge homotopies extend a square homotopy, with their literal boundary formulas retained.

  1. def OAI.HyperbolicObstruction.SquareBoundaryExtension.endpoint line 16
  2. def OAI.HyperbolicObstruction.SquareBoundaryExtension.other line 17
  3. def OAI.HyperbolicObstruction.SquareBoundaryExtension.face line 19
  4. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.face_closed line 22
  5. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.face_cover line 25
  6. structure OAI.HyperbolicObstruction.SquareBoundaryExtension.Data line 32
  7. def OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.onFace line 39
  8. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.agree line 46
  9. def OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.boundary line 72
  10. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.boundary_eq line 75
  11. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.boundary_initial line 85
  12. def OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.extend line 93

    Source documentation

    The complete square prism is extended, not merely its boundary class.

    def extend : C(I × (Fin 2 → I),X) :=
…
  13. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.extend_initial line 96
  14. lemma OAI.HyperbolicObstruction.SquareBoundaryExtension.Data.extend_edge line 98