OAI/Geometry/HyperbolicGroups/LoopSpaceReversal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reversing the spatial coordinate of an actual two-loop negates its genuine fundamental class in the compact-open loop space.

  1. def OAI.HyperbolicObstruction.LoopSpaceReversal.reverse line 16
  2. lemma OAI.HyperbolicObstruction.LoopSpaceReversal.reverse_apply line 19
  3. def OAI.HyperbolicObstruction.LoopSpaceReversal.cancel line 23

    Source documentation

    The cancellation homotopy is continuous jointly in both parameters and in the loop itself.

    def cancel (u : Path e e) : (Path.refl e).Homotopy
    (HSpaceFundamental.combinePath u (reverse b u)) where
…

    Mentions: OAI.HyperbolicObstruction.HSpaceFundamental.combinePath, OAI.HyperbolicObstruction.LoopSpaceReversal.reverse

  4. lemma OAI.HyperbolicObstruction.LoopSpaceReversal.reverse_class line 47