Transverse preimage theorem (source code)

= Transverse preimage theorem
{title2=$\operatorname{codim}_M f^{-1}(S)=\operatorname{codim}_N S$}

If $f:M\to N$ satisfies <transversality of a map to a submanifold> $S$, its nonempty preimage is an <embedded submanifold> of the displayed codimension. Choose a <slice chart for an embedded submanifold> around $f(p)$ in which $S$ is the zero set of the first $k$ coordinates. Their composition with $f$ has surjective derivative on its zero set, so the <regular level set theorem> gives a local embedded slice of dimension $\dim M-k$. These slices give the <subspace topology> and a compatible <smooth atlas> on the preimage. Its <tangent space> is
$$
T_pf^{-1}(S)=\{v\in T_pM:df_pv\in T_{f(p)}S\}.
$$