Having some difficulty with the following proposition,
Consider a $ C^\infty $ map between manifolds $ F:N \rightarrow M $ with $ \text{dim} \, N = \text{dim} \, M $, then $ F $ is locally invertible at some point $ p \in N $ if $ F_{*,p} : T_pN \rightarrow T_{F(p)}M $ is an isomorphism.
Now, I think I understand the general idea of how to show this, but am stuck on a finer point. Of course, the pushforward of a basis vector on $ T_pN $ given charts about $ p \in N $ and $ F(p) \in M $, $ (U, x^1,...,x^n) $ and $ (V,y^1,...,y^n) $ respectively, $$ F_{*,p} \bigg( \frac{\partial}{\partial x^i} \bigg|_p\bigg) = \sum_j^n \frac{\partial F^j}{\partial x^i}(p) \frac{\partial}{\partial y^j} \bigg|_{F(p)} \tag{1} $$ with $ F^j := y^j \circ F $. My intuition is to recall that for a linear operator $ T: \mathbb{R}^n \rightarrow \mathbb{R}^n $ such that $ T(v) = A v $ for $ v \in \mathbb{R}^n $ and $ A \in \text{GL}(n,\mathbb{R}) $, then $ T $ is invertible iff $ T $ is an isomorphism, in the hopes that similar logic can be applied to more abstract vector space transformations.
So, naturally, I want to argue that the pushforward of $ \partial / \partial x^i |_p $ is represented by the matrix $ \partial F^j / \partial x^i |_{F(p)} $, and the differential being an isomorphism is equivalent to the inverse matrix existing (which means that $ \text{det}[\partial F^j / \partial x^i |_{F(p)}] \neq 0 $), and thus $ F $ is invertible via the inverse function theorem on manifolds.
But $ F_{*,p} $ is then acting in a form like $ T(v) = A w = z $, with $ v \in T_pN $ and $ w,z \in T_{F(p)}M $. I'm unable to prove an analogue of the variant with $ T $ on $ \mathbb{R}^n $, because I can't just naively toss around $ A^{-1} $ on $ z $ to get an element in $ T_pN $, as $ w $ is in $ T_{F(p)}M $! The linear combination is of basis vectors $ \partial / \partial y^j $, and not $ \partial / \partial x^i $, which exist in different spaces, no? How can I prove that $ F_{*,p} $ is an isomorphism $ \iff \text{det}[\partial F^j / \partial x^i |_{F(p)}] \neq 0 $ to complete the proof?
Remember that $\frac{\partial F^j}{\partial x^k}(p):=\frac{\partial G^j}{\partial r^k}\phi (p)$ for $G:=\psi\circ F\circ \,\phi^{-1}$ where $\phi:=(x^1,\ldots ,x^n),\,\psi :=(y^1,\ldots ,y^n)$ and $r:=(r^1,\ldots ,r^n)$ is the Cartesian coordinate system in $\mathbb{R}^n$. Then as $\phi $ and $\psi $ are local diffeomorphisms of $M$ and $N$ respectively with $\mathbb{R}^n$ then $G:\mathbb{R}^n\to \mathbb{R}^n$ is an smooth map and $$ \det\left[\frac{\partial F^j}{\partial x^k}(p)\right]=\det\left[\frac{\partial G^j}{\partial r^k}\phi (p)\right] $$ Therefore if the determinant is not zero the derivative of $G$ at the point $\phi(p)$, that is $G_{*,\phi(p)}$, is an automorphism of $\mathbb{R}^n$ and so it is invertible. Now observe that $\phi_*$ and $\psi_*$ are isomorphisms (because they are assumed to be diffeomorphisms) and by the chain rule we have that $F_{*,p}=\psi _{*,F(p)}^{-1}\circ G_{*,\phi(p)}\circ \phi _{*,p}$, then as $F_{*,p}$ is composition of invertible linear maps its invertible.
By the other hand, if the determinant is zero then $G_{*,\phi(p)}$ is not invertible and so it kernel is not trivial, so there is some $x\in \mathbb{R}^n\setminus \{0\}$ such that $G_{*,\phi(p)}x=0$, and so $F_{*,p}((\phi_{*,p}) ^{-1}x)=0$, so $F_{*,p}$ is not invertible because, being $\phi_*$ an isomorphism, $(\phi_{*,p}) ^{-1}x\neq 0$ when $x\neq 0$.∎