Recall the inverse function theorem from multivariable calculus: if is a map defined on an open region , and if the Jacobian of has maximal rank at a point then there is some neighborhood of so that the restriction is a diffeomorphism. This is slightly different than how we stated it before, but it’s a pretty straightforward translation.
Anyway, this generalizes immediately to more general manifolds. We know that the proper generalization of the Jacobian is the derivative of a smooth map , where is an open region of an -manifold and is another -manifold. If the derivative has maximal rank at , then there is some neighborhood of for which is a diffeomorphism.
Well, this is actually pretty simple to prove. Just take coordinates at and at . We can restrict the domain of to assume that is entirely contained in the coordinate patch. Then we can set up the function .
Since has maximal rank, so does the matrix of with respect to the bases of coordinate vectors and , which is exactly the Jacobian of . Thus the original inverse function theorem applies to show that there is some on which is a diffeomorphism. Since the coordinate maps and are diffeomorphisms we can write for some , and conclude that is a diffeomorphism, as asserted.