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?