OAI/Geometry/HyperbolicGroups/SquarePathFilling.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

A literal square with prescribed boundary paths, constructed from a relative path homotopy by an explicit compact quotient.

  1. def OAI.HyperbolicObstruction.SquarePathFilling.low line 15
  2. def OAI.HyperbolicObstruction.SquarePathFilling.high line 16
  3. lemma OAI.HyperbolicObstruction.SquarePathFilling.bounds line 17
  4. lemma OAI.HyperbolicObstruction.SquarePathFilling.sum line 26
  5. lemma OAI.HyperbolicObstruction.SquarePathFilling.gap_pos line 31
  6. lemma OAI.HyperbolicObstruction.SquarePathFilling.low_continuous line 34
  7. lemma OAI.HyperbolicObstruction.SquarePathFilling.high_continuous line 35
  8. def OAI.HyperbolicObstruction.SquarePathFilling.quotient line 39

    Source documentation

    Horizontal parameter selects a broken boundary path; vertical parameter runs from its common source to its common target.

    def quotient : C(I × I,I × I) where
…
  9. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_sum line 60
  10. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_fiber line 65
  11. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_surjective line 88
  12. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_isQuotientMap line 125
  13. lemma OAI.HyperbolicObstruction.SquarePathFilling.homotopy_fiber line 131
  14. def OAI.HyperbolicObstruction.SquarePathFilling.fill line 139

    Source documentation

    The actual square filling, with no extension assumption.

    def fill (H : (p.trans r).Homotopy (q.trans s)) : C(I × I,X) where
…
  15. lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_quotient line 149
  16. def OAI.HyperbolicObstruction.SquarePathFilling.half line 153
  17. def OAI.HyperbolicObstruction.SquarePathFilling.upper line 155
  18. lemma OAI.HyperbolicObstruction.SquarePathFilling.low_half line 157
  19. lemma OAI.HyperbolicObstruction.SquarePathFilling.high_half line 159
  20. lemma OAI.HyperbolicObstruction.SquarePathFilling.low_upper line 161
  21. lemma OAI.HyperbolicObstruction.SquarePathFilling.high_upper line 163
  22. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_bottom line 166
  23. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_left line 169
  24. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_right line 172
  25. lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_top line 175
  26. lemma OAI.HyperbolicObstruction.SquarePathFilling.trans_half line 179
  27. lemma OAI.HyperbolicObstruction.SquarePathFilling.trans_upper line 185
  28. lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_bottom line 192
  29. lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_left line 196
  30. lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_right line 200
  31. lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_top line 204