OAI/Geometry/HyperbolicGroups/CubicalHomotopyExtension.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Explicit prism retraction proving the cubical homotopy extension geometry. All maps use the actual interval and product/subspace topologies.

  1. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius line 16
  2. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius_continuous line 18
  3. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius_nonneg line 22
  4. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius_le_one line 25
  5. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.coord_le_radius line 34
  6. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius_eq_one_iff line 38
  7. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator line 65
  8. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator_ge_half line 67
  9. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator_pos line 72
  10. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator_le_one line 75
  11. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator_continuous line 80
  12. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.retractTime line 85
  13. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.retractCube line 96
  14. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.retractTime_continuous line 108
  15. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.retractCube_continuous line 114
  16. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.radius_retractCube line 122
  17. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.bottomSides line 134

    Source documentation

    The bottom of the prism together with all its vertical sides.

    def bottomSides : Set (I × (N → I)) := {tx | tx.1 = 0 ∨ tx.2 ∈ Cube.boundary N}
  18. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.retraction_mem line 136
  19. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.retraction line 154

    Source documentation

    Literal continuous retraction of the prism to bottom and sides.

    def retraction : C(I × (N → I),bottomSides (N := N)) where
…

    Mentions: OAI.HyperbolicObstruction.CubicalHomotopyExtension.bottomSides

  20. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.denominator_eq_one line 158
  21. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.retraction_fixed line 168
  22. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.boundary_isClosed line 182
  23. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.sideGlueRaw line 191

    Source documentation

    Glue the prescribed initial map and boundary homotopy on the closed bottom-and-sides subspace.

    def sideGlueRaw (f : C(N → I,X)) (H : C(I × Cube.boundary N,X))
    (tx : I × (N → I)) : X :=
…
  24. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.sideGlueRaw_bottom line 196
  25. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.sideGlueRaw_side line 206
  26. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.sideGlueRaw_continuousOn line 211
  27. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.sideGlue line 236
  28. def OAI.HyperbolicObstruction.CubicalHomotopyExtension.extend line 243

    Source documentation

    Genuine cubical homotopy extension, constructed by the explicit prism retraction. No extension or cellular-approximation premise is used.

    def extend (f : C(N → I,X)) (H : C(I × Cube.boundary N,X))
    (hH : ∀ x : Cube.boundary N, H (0,x) = f x) : C(I × (N → I),X) :=
…
  29. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.extend_bottom line 247
  30. lemma OAI.HyperbolicObstruction.CubicalHomotopyExtension.extend_side line 254