# Differentiability of a map to the free loop space

While reading Morse theory, closed geodesics, and the homology of free loop spaces, the author claims the following:

Given the $S^{n-1} \hookrightarrow Y_1 \rightarrow T^1S^n$ bundle over $T^1S^n$, which has fibers over $(x,v)$ being the $(n-1)$-dimensional equator which is orthogonal to $v$ and passing through $x$, and defining the map $$\phi: Y_1 \rightarrow \Lambda S^n,$$ where $\Lambda S^n$ is the free loop space, which takes a point $(x,v,y)$ and sends it to the circle in the sphere which is tangent to $v$ and arrives orthogonally on the equator "$S^{n-1}$" at $y$, then $\phi$ is an embedding near $\phi^{-1}(K)$, where $K$ is the first non-trivial critical energy level (that is, it is not the constant maps), mapping $\phi^{-1}(K)$ diffeomorphically in $K$.

He states that one can directly check the above statement. However, I don't see how this would be a quick check. I have at my disposal few lemmas about differentiability of functions to $\Lambda S^n$ (for example, Lemma of Palais, c.f. Klingenberg). So my idea would be to use the local charts for $\Lambda S^n$, but this seems quite laborious, and I'm not sure if the author had this in mind. Is there some general theorem being used? Otherwise, how can one show the above statement?

• A map to the loop space is smooth if and only if it maps smooth curves to smooth curves. A smooth curve in the Loop space over $S^n$ is just a map from a cylinder to $S^n$ (plus some base condition if you want). This should give you enough tools to verify the statement. – Matthias Ludewig Jan 18 '16 at 19:04