The local map generated by a first- or second-kind generating function is a canonical $C^2$ local diffeomorphism

Given: The first- or second-kind generating data $S$, the maps $\mathrm{\Psi }$, $\mathrm{\Theta }$ and $C$ introduced in Generating functions of the first and second kind for a local canonical map, and a point $(q_{\ast },Q_{\ast })$ resp. $(q_{\ast },P_{\ast })$ as in that definition.

Local diffeomorphism data (Generating functions of the first and second kind for a local canonical map, The Euclidean inverse function theorem): $\mathrm{\Psi }(q,Q)=(q,S_q(q,Q))$ has invertible derivative because $\det S_{qQ}\mathrm{\ne }0$ and, in the second-kind case, $(q,P)\mapsto (q,S_q(q,P))$ has invertible derivative because $\det S_{qP}\mathrm{\ne }0$; the generated map $C$ is obtained by composing the $C^2$ local inverse of that map with the $C^2$ map $(q,Q)\mapsto (Q,-S_Q(q,Q))$ resp. $(q,P)\mapsto (S_P(q,P),P)$, so $C$ is a $C^2$ map. Its derivative is shown invertible in the proof before the canonical-diffeomorphism test is applied.

The $\mathrm{\Psi }$-$\mathrm{\Theta }$ conjugation: in the first-kind case, with $W$ a suitable neighbourhood of $(q_{\ast },Q_{\ast })$ and $\mathrm{\Psi }(q,Q)=(q,p)$, the map $\mathrm{\Theta }(q,Q):=(Q,-S_Q(q,Q))$ satisfies $C\circ \mathrm{\Psi }=\mathrm{\Theta }$ on $W$, because the inverse of $\mathrm{\Psi }$ maps $(q,p)$ back to $(q,Q)$ and $C(q,p)=(Q,-S_Q(q,Q))$; in particular $C^{\ast }\tau ={\mathrm{\Psi }}^{-\star }{\mathrm{\Theta }}^{\ast }\tau$ for every two-form $\tau$ on the target. In the second-kind case the same holds with $\mathrm{\Psi }(q,P)=(q,p)$ and $\mathrm{\Theta }(q,P)=(S_P(q,P),P)$.

Derivative computation (Directional derivatives and partial derivatives of a map $U\subseteq {\mathbb{R}}^m\to {\mathbb{R}}^n$, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, The Hessian of a $C^2$ scalar field is symmetric): in the first-kind case, ${\mathrm{\Psi }}^{\ast }(dq\wedge dp)={\sum }_{i,j}{\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{q}^i\mathrm{\partial }{Q}^j(q,Q)d{q}^i\wedge d{Q}^j$ because $dp=S_{qq}dq+S_{qQ}dQ$ on $W$; and ${\mathrm{\Theta }}^{\ast }(dQ\wedge dP)={\sum }_{i,j}{\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{q}^i\mathrm{\partial }{Q}^{j}d{q}^i\wedge d{Q}^j$ because $P=-S_Q$ gives $dP=-S_{QQ}dQ-S_{Qq}dq$ on $W$ and the mixed partials ${\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{Q}^j\mathrm{\partial }{q}^i={\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{q}^i\mathrm{\partial }{Q}^j$ agree. In the second-kind case, $dp=S_{qq}dq+S_{qP}dP$ gives ${\mathrm{\Psi }}^{\ast }(dq\wedge dp)={\sum }_{i,j}{\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{q}^i\mathrm{\partial }{P}^{j}d{q}^i\wedge d{P}^j$, and $dQ=d(S_P)=S_{Pq}dq+S_{PP}dP$ gives ${\mathrm{\Theta }}^{\ast }(dQ\wedge dP)={\sum }_{i,j}{\mathrm{\partial }}^{2}S\mathrm{/}\mathrm{\partial }{P}^j\mathrm{\partial }{q}^{i}d{q}^i\wedge d{P}^j$, the same formula.

Finite-regularity coordinate calculus (Finite-regularity differential forms, Hamiltonian fields and canonical maps in phase charts, The Hessian of a $C^2$ scalar field is symmetric): for the $C^3$ function $S$, $d(dS)=0$ because the coefficients of this two-form are differences of equal mixed second partials. Pointwise pullbacks commute with sums and wedge products by their alternating multilinear definition, and with composition by the chain rule.