Consider the following claim:

Let $p:M \to N$ be a (surjective) submersion of finite-dimensional smooth manifolds. Let $J$ denote one of $[0,1],\ [0,1),\ (0,1]$. Then $p_*:M^J \to N^J$ is a submersion of Frechet manifolds, where $X^J$ denotes the usual manifold of smooth paths in $X$.

The intuition is that given a lift of a path $\gamma$ through $p$, one can find a neighbourhood $U$ of the image of $\gamma$ and a neighbourhood $V$ of the image of the lift such that for every path in $U$ one can smoothly choose a lift to $V$.

Here I suppose we need a submersion of Frechet manifolds to be a map that admits local sections through every point in the domain, if that is the 'correct' notion of submersion in that setting (certainly not the 'surjective on tangent spaces' version).

I think the proof would use the characterisation of submersions as maps
which look locally (on both the *domain* and codomain) like projections
$U \times \mathbb{R}^n \to U$, and the existence of good open covers with smooth
contractions.

I think I'm able to prove that there are continuous sections through every point in the domain, thinking of everything as a topological space, and using the compact-open topology on the mapping spaces. But I don't know off the top of my head that the compact-open topology on the space of smooth paths is the same as the topology inherited from the Frechet manifold structure. (My guess is that it is.)

My question: is the claim true?

As Andrew Stacey points out in the comments, the mapping space is not a manifold for non-compact intervals. However, I think I really only need maps which have all derivatives uniformly bounded (but a different bound for each derivative!). Since the topology on the mapping space for compact intervals uses uniform convergence, I'm betting that this set has the structure of a Frechet manifold.

Question 2: am I right?

Question 1': if so, is the claim true for this (putative) map of Frechet manifolds?

musthave (sequential) compactness. The non-compact end can wander all over the manifold and that destroys the possibility of any sort of nice local structure. In the compact-open topology then locally, I cannot know anything about the open end because I can only know what's happening on a compact set. So two nearby paths need not be physically near at all. You can change the topology to get a manifold, but then you get uncountably many components (according to what the open end is doing). $\endgroup$2more comments