Solution (source code)

= Solution

A <local isometry> preserves the <Levi-Civita connection> and hence <geodesics>, as well as the lengths of lifted curves. We first show that a complete source permits finite-length paths to lift all the way to their endpoints. Begin lifting a piecewise smooth path $c:[0,1]\to N$ from any chosen point above $c(0)$, using local inverse maps. If its lift is defined only up to a maximal $b\leq1$, then
$$
d_M(\widetilde c(s),\widetilde c(t))\leq\operatorname{length}(c|_{[s,t]})\longrightarrow0
\quad\text{as }s,t\uparrow b.
$$
Completeness gives a limit point in $M$. A local inverse at that point continues the lift, including its endpoint. Thus such a finite obstruction is impossible. Connectedness of $N$ and piecewise smooth paths from $f(p)$ to any target point prove that $f$ is onto; no prior completeness of $N$ is used in this step.

Now lift the initial position and velocity of any <geodesic> in $N$. The resulting <geodesic> in $M$ exists for all real time by <Hopf-Rinow theorem>. Its image extends the original target <geodesic> by uniqueness of the <geodesic> initial-value problem. Hence $N$ is geodesically complete, and therefore complete.

\b[The converse is false for a general local <isometry>], even an onto one. Give the interval $(0,4\pi)$ its ordinary metric and map it to the unit circle by $t\mapsto e^{it}$. This is an onto <local isometry> to a complete circle, but the sequence $t_j=1/j$ is Cauchy in the interval and has no limit there. It is not a <covering map>: the identity point of the circle has only one preimage, whereas nearby points have two.

\b[The converse holds for a Riemannian covering.] If $f$ is also a <covering map> and $N$ is complete, every target <geodesic> defined on $\mathbb R$ lifts globally with any specified initial point. A <local isometry> makes that lift a <geodesic>. Its initial velocity can be any prescribed source velocity because $df$ is an isomorphism. Thus all source <geodesics> extend for all time, and $M$ is complete by the <Hopf-Rinow theorem>.