Restriction of local diffeomorphism to a neighbourhood of a submanifold is injective Question. Let $\varphi : M \to N$ be a local diffeomorphism of smooth manifolds and $S \subset M$ a smooth submanifold such that $\varphi|_S: S \to N$ is an embedding. Is there a neighbourhood $U$ of $S$ in $M$ such that $\varphi|_U$ is injective?
My guess is that we can achieve this by taking a neighbourhood $U$ which deformation retracts onto $S$. This can be done, for example, by taking a tubular neighbourhood, i.e. a diffeomorphism from a neighbourhood of the zero section in the normal bundle of $S$ to a neighbourhood of $S$ in $M$, and contracting by scalar multiplication. Then, there is perhaps an argument using path liftings, but I'm unsure how to do this. If $\varphi(p) = \varphi(q)$, we could maybe argue that there is a path from $p$ to $q$ which maps to a contractible loop in $N$ and somehow use this to show that $p = q$? Since $\varphi$ is a priori not a covering map, I'm not sure if this is a good approach.
 A: As you've suggested, this can be proven using tubular neighborhoods.
We can choose a Riemannian metric $g$ on $N$ and equip $M$ with the pullback metric $\varphi^*g$. With these metrics, we can consider normal bundles as subbundles $NS\subseteq TM|_S$ and $N\varphi(S)\subseteq TN|_{\varphi(S)}$, and $d\varphi|_{NS}:NS\to N\varphi(S)$ is then an isomorphism.
By the tubular neighbor theorem, there are open neighborhoods $U\subseteq NS$ and $V\subseteq M$ (with $U$ fiberwise star-shaped) and a diffeomorphism $\psi:U\to V$ defined by $\psi(v)=\gamma_v(1)$, where $\gamma$ is the geodesic with initial velocity $v\in NS$. Note that $\psi$ maps the zero section of $NS$ to $S$.
There likwise exist $U'\subseteq N\varphi(S)$, $V'\subseteq N$ and $\psi':U'\to V'$ with the same properties, and since $\varphi$ maps geodesics onto geodesics, $\psi'(d\varphi(v))=\varphi(\psi(v))$ where both sides are well defined.
Since $U'\cap d\varphi(U)$ contains the zero section of $N\varphi(S)$, the map
$$
\psi'|_{U'\cap d\varphi(U)}\circ d\varphi|_{U\cap d\varphi^{-1}(U')}\circ\psi^{-1}|_{V\cap\psi(d\varphi^{-1}(U'))}
$$
is a diffeomorphism between open sets containing $S$ and $\varphi(S)$, and is equal to $\varphi$ on its domain.
