My book is An Introduction to Manifolds by Loring W. Tu.
I think that since diffeomorphisms are equivalent to surjective smooth embeddings, I think this is the same as proving an injective local diffeomorphism is a smooth embedding (I understand "image is submanifold and diffeomorphism onto its image" is an equivalent definition of a smooth embedding) which is asked here and here (and here in the continuous case), but I would like a verification of my own proof:
Let $M$ and $N$ be smooth manifolds of respective dimensions $m$ and $n$. Let $F: N \to M=F(N)$ be a bijective smooth map. Suppose $F$ is a local diffeomorphism. Let us show that $F^{-1}: M \to N$ is smooth, using Definition 6.5, to show that $F$ is actually a diffeomorphism.
Let $U$ be open in $N$. I'll denote by
$F|_U$ as the domain-restriction $F|_U:U \to M$,
$\tilde{F|_U}$ as the range-restriction $\tilde{F|_U}:U \to F(U)$
$G$ as the inverse of $\tilde{F|_U}$, i.e. $G := (\tilde{F|_U})^{-1}: F(U) \to U$.
- Equivalently, $G = \tilde{F^{-1}|_{F(U)}}: F(U) \to U$, the range-restriction of the domain-restriction $F^{-1}|_{F(U)}: F(U) \to N$ of $F^{-1}: M \to N$
I understand that the "$\varphi \circ F^{-1} \circ \psi^{-1}$" in Definition 6.5 refers to "$\varphi \circ G \circ \psi^{-1}$"
For all $F(p) \in M$, with $p \in N$, we must find a chart $(U, \varphi)$ about $p$ in $N$ and a chart $(V, \psi)$ about $F(p)$ in $M$ such that $$\varphi \circ G \circ \psi^{-1}: \psi(F(U) \cap V) \to (\varphi \circ G)(F(U) \cap V)$$ is smooth about the point $\psi(F(p))$ (its value at $\psi(F(p))$ is $\varphi(p)$).
Let us now use the local diffeomorphism property: For all $p \in N$, there exists a neighborhood $U_p$ of $p$ in $N$ such that for the domain-restriction $F|_{U_p}: U_p \to M$ and the range-restriction $\tilde{F|_{U_p}}: U_p \to F(U_p)$, $F(U_p)$ is open in $M$ and $\tilde{F|_{U_p}}$ is a diffeomorphism.
I'm not sure if $U_p$ has a coordinate map $\gamma$ that makes $(U_p,\gamma)$ into a chart, but since $U_p$ is an open subset of $N$, $U_p$ can be made into a smooth manifold. Viewing $p \in U_p$, there exists a chart $(A_p,\varphi_A)$ about $p$ in $U_p$. I know $A_p$ is open in both $U_p$ and $N$, and I think $(A_p,\varphi_A)$ is also a chart about $p$ in $N$. (If relevant: I guess we use that open subsets are equivalent to regular submanifolds of codimension zero.)
$n=m$ because
$n = \dim N = \dim U_p = \dim F(U_p) = \dim M = m$, where
$\dim F(U_p)$ is defined because $F(U_p)$ becomes a manifold because $F(U_p)$ is an open subset of $M$ (from (5))
$\dim U_p = \dim F(U_p)$ because of (3) in another post
I'll choose $(U, \varphi) = (A_p,\varphi_A)$ and $(V, \psi) = (G^{-1}(A_p), \varphi_A \circ G)$. This works because
8.1 $$\varphi \circ F^{-1} \circ \psi^{-1} = \varphi \circ G \circ \psi^{-1} = \varphi_A \circ G \circ (\varphi_A \circ G)^{-1}$$
$$ = \varphi_A \circ G \circ G^{-1} \circ \varphi_A^{-1} = \varphi_A \circ \varphi_A^{-1}$$
8.2 $\psi(F(U) \cap V) = (\varphi_A \circ G)(F(A_p) \cap G^{-1}(A_p)) = (\varphi \circ G)(F(U) \cap V)$ (which turns out to be equal to $\varphi_A(A_p)$)
8.3 By (8.2) and (7), it makes sense to say that (8.1) shows that $\varphi \circ F^{-1} \circ \psi^{-1}$ is an identity map on an open subset of $\mathbb R^m$.
Identity maps on open subsets of $\mathbb R^m$ are smooth.
Therefore, by (8) and (9), $F^{-1}$ is smooth.
Therefore, by (10) and (1), $F$ is a diffeomorphism.