I'm trying to prove the following claim:
Let $F\colon M \to N$ be a differentiable application beetween $C^\infty$ manifolds. Then the differential $\text dF_p\colon T_p M \to T_{F(p)}N$ is injective if and only if the pullback $F_p^*\colon C^\infty _N (F(p))\to C^\infty _M (p)$ is surjective.
Where $C^\infty _S (q)$ are the germs in $q$, $F_p^*(\mathbf g)=\mathbf g \circ F$ and $\text dF_p (X)=X\circ F_p ^*$.
I'll use Einstein's convention on summations. Let $(\varphi = (x^1,x^2,\dots,x^n),U)$ be a local chart in $p$.
Sufficiency: Proof by contrapositive: suppose that $\text d F_p(X^i \partial _i |_p)=O$ and $X^k\neq 0$. Then for all $\mathbf g \in C^\infty _N (F(p))$ $$0=\text d F_p(X^i \partial _i |_p)(\mathbf g)=X^i \partial _i |_p(F_p ^*(\mathbf g)).$$ This shows that $\mathbf x ^k$ is not in the image of $F_p ^*$, hence if $F_p^*$ is surjective then $\text d F _p$ is injective. []
Now for the converse, I was reasoning on these lines: if $F_p ^* (\mathbf h)\neq \mathbf g$ for all $\mathbf h \in C^\infty _N (F(p))$ and for some $\mathbf g \in C^\infty _M (p)$, then we can consider the ideal $$I=\{ \mathbf g \cdot \mathbf f_0 | \mathbf f _0 \in C^\infty _M (p)\}.$$ It is easily seen that $$\text {Im}F_p ^*\cap I= \{\mathbf 0 \}.$$ Now, if I could find a derivation such that $X(\mathbf g)=1$ and $X(C^\infty _M (p) - I)=\{0\}$ this would be done. My problem is to find such $X$.
Since it is not restrictive to assume $\mathbf g(p)=0$, more generally a derivation would act on $I$ in this way: $$X(\mathbf f)=X(\mathbf g \mathbf f _0)=X(\mathbf g)\mathbf f(p),$$ however I'm not sure if I can use this fact in any way.
Any help is appreciated; I'd prefer to complete my proof, but also a different one would be OK.