We can also recall the implicit function theorem. This is less directly generalizable to manifolds, since talking about a function is effectively considering a manifold with a particular product structure: the product between the function’s domain and range.
Still, we can go back and clean up not only the statement of the implicit function theorem, but its proof, as well. And we can even extend to a different, related statement, all using the inverse function theorem for manifolds.
So, take a smooth function , where with . Suppose further that has maximal rank at a point . If we write for the projection onto the first components of , then there is some coordinate patch of around so that in that patch.
This is pretty much just like the original proof. We can clearly define to agree with in its first components and just to copy over the th component for . That is,
Then , and the Jacobian of is
After possibly rearranging the arguments of , we may assume that the matrix in the upper-left has nonzero determinant — has rank at , by assumption — and so the Jacobian of also has nonzero determinant. By the inverse function theorem, has a neighborhood of on which it’s a diffeomorphism . Thus on we conclude
This is basically the implicit function theorem from before. But now let’s consider what happens when . Again, we assume that has maximal rank — this time it’s — at a point . If we write for the inclusion of into the first components of , then I say that there is a coordinate patch around so that in a neighborhood of .
This time, we take the product and define the function by
Then , and the Jacobian of at is
Just as before, by rearranging the components of we can assume that the determinant of the matrix in the upper-left is nonzero, and thus the determinant of the whole Jacobian is nonzero. And thus is a diffeomorphism on some neighborhood . We let be the image of this neighborhood, and write . Thus on some neighborhood we conclude
Either way, the conclusion is that we can always pick local coordinates on the larger-dimensional space so that is effectively just a simple inclusion or projection with respect to those coordinates.