Why is a differential equation a submanifold of a jet bundle?

I'm reading The geometry of jet bundles by D.J Saunders and struggle with the definition of a differential equation 6.2.23. on page 203.

First of all, Saunders introduces a differential operator determined by a bundle map: Let $(E, \pi, M)$ and $(H, \rho, M)$ be bundles and let $(f, id_M)$ a bundle morphism between the jet-bundle $J^k(\pi)$ and $H$. This means, that $f: J^k(\pi) \to H$ is a smooth map that respects the projections. The differential operator determined f is the map $D_f: \Gamma_{loc} (\pi) \to \Gamma_{loc}(\rho)$ taking a local section $\phi$ of $\pi$ to the local section $D_f(\phi)$ of $\rho$ with $D_f(\phi) (p) = f(j^k_p \phi)$.

For a differential operator $D_f$ determined by $f$ and a local section $\chi$ of $\rho$ he than defines the differential equation determindes by $D_f$ and $\chi$ to be the submanifold $$S_{f; \chi} = \lbrace j^k_p \phi: f(j^k_p \phi) = \chi (p) \rbrace \subset J^k \pi $$

I can see, why the definition of the set $S_{f; \chi}$ defines a differential equation in a rather intuitive way. Now my question is: Why is this set in deed a submanifold?

I guess there is a nice widly known theorem on the core of the theory on fibre bundles which I unfortunatly do not know. So if anybody could point out a reference to such a theorem, I would be grateful!


Let $\bar \chi : J^k \pi \to H$ be the composition of $\chi$ with the projection of $J^k \pi$; i.e. $\bar \chi (\xi_p) = \chi(p)$. Then since $$S_{f;\chi} = \{\xi_p \in J^k \pi : f(\xi_p) = \bar \chi(\xi_p) \},$$ a slight generalization of the regular value theorem tells us that it is a submanifold if $Df - D\bar\chi$ is surjective everywhere in $S_{f;\chi}$. I believe you need some additional assumption to make this true - otherwise standard examples of non-manifold level sets should easily extend to this setting.

Since $\bar\chi$ is constant in the vertical direction, it suffices for the restriction of $Df$ to the vertical bundle to be surjective; so you probably want to require this of your differential operator.