OAI/Geometry/HyperbolicGroups/PathHomotopyTopology.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The genuine compact-open path space realizes relative homotopies as paths. This is the two-dimensional path-space interface used for cellular obstructions.

  1. def OAI.HyperbolicObstruction.PathHomotopyTopology.fromHomotopy line 15
  2. def OAI.HyperbolicObstruction.PathHomotopyTopology.toHomotopy line 21
  3. lemma OAI.HyperbolicObstruction.PathHomotopyTopology.fromHomotopy_apply line 32
  4. lemma OAI.HyperbolicObstruction.PathHomotopyTopology.toHomotopy_apply line 34
  5. def OAI.HyperbolicObstruction.PathHomotopyTopology.equiv line 38

    Source documentation

    No homotopy classes are collapsed by this change of representation.

    def equiv : (p.Homotopy q) ≃ Path p q where
…
  6. lemma OAI.HyperbolicObstruction.PathHomotopyTopology.joined_iff_homotopic line 44