English
Let i be an index in N. For any p and q in the space of N-dimensional generalized loops at x, if there exists a homotopy H between the i-th loops (toLoop i p) and (toLoop i q), then there is a corresponding higher-dimensional homotopy F: I × I^N → X realizing a homotopy between p and q. In other words, a homotopy between i-th loops yields a (n+1)-dimensional path in X describing a homotopy between p and q.
Русский
Пусть i — элемент N. Для любых p и q из пространства n-мерных обобщённых петлей GenLoop N X x, если существует гомотопия H между i-й петлёй (toLoop i p) и (toLoop i q), то существует соответствующая гомотопия высшего размера F: I × I^N → X, которая реализует гомотопию между p и q. Другими словами, гомотопия по координате i порождает (n+1)-мерную путь в X, описывающую гомотопию между p и q.
LaTeX
$$$\\mathrm{HomotopyFrom}(i; p, q; H) \\in C(I \\times I^N, X)$, where $H$ is a Path.Homotopy $(\\mathrm{toLoop}\\; i\\; p) \\;\\mathrm{Homotopy} \\; (\\mathrm{toLoop}\\; i\\; q)$ and $p, q \\in (\\mathrm GenLoop\\ N X x).\\mathrm{Elem}$. The map is constructed by composing appropriate currying/uncurrying operations along the $i$-th coordinate and the Subtype projection, yielding a higher-dimensional path in $X$.$$
Lean4
/-- The converse to `GenLoop.homotopyTo`: a homotopy between two loops in the space of
`n`-dimensional loops can be seen as a homotopy between two `n+1`-dimensional paths. -/
@[simps!]
def homotopyFrom (i : N) {p q : Ω^ N X x} (H : (toLoop i p).Homotopy (toLoop i q)) : C(I × I^N, X) :=
(ContinuousMap.comp ⟨_, ContinuousMap.continuous_uncurry⟩
(ContinuousMap.comp ⟨Subtype.val, by fun_prop⟩ H.toContinuousMap).curry).uncurry.comp <|
(ContinuousMap.id I).prodMap (Cube.splitAt i)
