Symplectic neighborhood theorem

By [F1], $df\oplus F:T{M}_0{\mathrm{\mid }}_{S_0}\to T{M}_1{\mathrm{\mid }}_{S_1}$ is a symplectic vector-bundle isomorphism: the two summands are symplectically orthogonal and each summand map is symplectic. We need tubular maps with a specified vertical derivative, not merely the existence clause of [F2]. Rerun its explicit proof using the smooth direct-sum complement $C_j=N^{{\omega }_j}{S}_j$ in place of the metric-orthogonal complement. In the proof's Euclidean-retraction construction, the map on $C_j$ has the form $(p,v)\mapsto j_j^{-1}{R}_j(j_j(i_j(p))+d{j}_j(v))$; its differential at $(p,0)$ is $(u,v)\mapsto d{i}_j(u)+v$. The local-frame topology, inverse-function argument, and continuous variable-radius shrinking there use only injectivity of $d{j}_j{\mathrm{\mid }}_{C_j}$ and $T{M}_j{\mathrm{\mid }}_{S_j}=T{S}_j\oplus C_j$, so they apply to this complement unchanged. Write the resulting tubular maps as ${\mathrm{\Psi }}_j$ on neighbourhoods in $C_j$. Then $h={\mathrm{\Psi }}_1\circ F\circ {\mathrm{\Psi }}_0^{-1}$ is a diffeomorphism of neighbourhoods extending $f$, and its differential along $S_0$ is exactly $df\oplus F$.

Consequently $h^{\ast }{\omega }_1$ and ${\omega }_0$ agree as bilinear forms on all of $T{M}_0{\mathrm{\mid }}_{S_0}$. Their convex interpolation ${\mathrm{\Omega }}_t=(1-t){\omega }_0+t{h}^{\ast }{\omega }_1$ is symplectic near $S_0$ after shrinking, because it equals ${\omega }_0$ on $S_0$ for every parameter and nondegeneracy is open. Put $\alpha =h^{\ast }{\omega }_1-{\omega }_0$. By [F3], $\alpha =d\sigma$ for a one-form $\sigma$ whose first jet vanishes on $S_0$. Solve ${\iota }_{X_t}{\mathrm{\Omega }}_t=-\sigma$. The inverse bundle maps ${\mathrm{\Omega }}_t^{-\mathrm{♭}}$ are smooth, so $X_t$ also has vanishing first jet on $S_0$.

The affine formula ${\mathrm{\Omega }}_t=(1-t){\omega }_0+t{h}^{\ast }{\omega }_1$ is smooth for all real $t$ and equals ${\omega }_0$ as a full tensor at each point of $S_0$ for every $t$. For each $p\in S_0$, compactness of $[0,1]$ and openness of nondegeneracy give a spatial neighbourhood $U_p$ and an open time interval $I_p\supset [0,1]$ on which ${\mathrm{\Omega }}_t$ is nondegenerate. Thus $X_t=-{\mathrm{\Omega }}_t^{-\mathrm{♭}}\sigma$ is genuinely defined on an open time domain near $([0,1],p)$, as required by the local-evolution supplier in [F4]. Since $X_t$ and its first derivative vanish along $S_0$, the constant solutions and variational equation give a time-one evolution $g$ on some neighbourhood of each $p$, fixing $S_0$ with $dg{\mathrm{\mid }}_{T{M}_0{\mathrm{\mid }}_{S_0}}=I$. Uniqueness glues these local evolutions after shrinking their spatial domains; no uniform time collar is needed when $S_0$ is noncompact. The pullback differentiation equation in [F4] gives $g^{\ast }{h}^{\ast }{\omega }_1={\omega }_0$. Thus $h\circ g$ is the required symplectomorphism and induces the prescribed $F$ on symplectic normal bundles. For empty $S_0$, take empty neighbourhoods and the empty map.