OAI/Topology/CoarseAssembly/WindingHomotopy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit homotopy from a lifted loop to its winding power

  1. def OAI.CoarseAssembly.circleDegree line 14

    Source documentation

    The degree-n self-map of the additive circle.

    def circleDegree (n : ℤ) : C(WindingCircle, WindingCircle) :=
…

    Mentions: OAI.CoarseAssembly.WindingCircle

  2. theorem OAI.CoarseAssembly.windingCircle_intCast line 17
  3. def OAI.CoarseAssembly.windingInterpolation line 23

    Source documentation

    Straight-line interpolation of the real lift with t ↦ n*t.

    def windingInterpolation (n : ℤ) (L : Path (0 : ℝ) (n : ℝ)) (s : unitInterval) :
    Path (0 : WindingCircle) 0 where
…

    Mentions: OAI.CoarseAssembly.WindingCircle

  4. def OAI.CoarseAssembly.windingInterpolationMap line 34
  5. theorem OAI.CoarseAssembly.windingInterpolationMap_continuous line 38
  6. def OAI.CoarseAssembly.windingHomotopy line 60