Let $G$ be a Lie group, let $\pi_P:P\to M$ and $\pi_Q:Q\to N$ be smooth right principal $G$-bundles, and let $F$ be a smooth left $G$-manifold. Let $f:M\to N$ be a smooth map and let $\Phi:P\to Q$ be a smooth principal $G$-bundle morphism covering $f$, meaning that
is a well-defined smooth map of associated bundles covering $f$. Equivalently, if $\rho_P:P\times_G F\to M$ and $\rho_Q:Q\times_G F\to N$ are the associated bundle projections, then