Implicit function theorems give sufficient conditions for the existence of a differentiable inverse of a germ of a differentiable map of smooth manifolds at a point . The invertibility is trivially equivalent to the statement that the germ is a local diffeomorphism of some neighborhood of to some neighborhood of . If it is invertible, then we can consider the tangent map . If is locally invertible with differentiable inverse, then for all in some neighborhood of the functoriality of implies that and alike for at , demonstrating that must then be invertible. The inverse function theorem says that the invertibility of is in fact sufficient for the invertibility of the germ, which is then automatically differentiable.
This is the theorem stated in the Idea section; the differentiable germ is assumed to be of class (continuously differentiable). The statement is local, so one can consider it in charts, hence the proof reduces to the case of .
Let be a smooth map of smooth manifolds. A point is a regular value of if for every point the differential is an epimorphism. The implicit function theorem asserts that is a smooth submanifold of and the tangent bundle globally splits as where .
More generally, if is a submanifold, we say that the map is transversal along if for every point there is an equality
In particular, is transveral along every regular value . The implicit function theorem asserts that the preimage is a smooth submanifold of , the normal bundle is isomorphic to , and the differential exhibits the fiberwise isomorphism .
L. H. Loomis, S. Sternberg, Advanced calculus, 1968, 1990 (3.11 in 1990 edition)
S. Lang, Analysis I
Various applications and related theorems can be found in chapter 5: Local and tangential properties of
An invariant global statement on manifolds is at page 44 of
Elementary course notes of the case in (mainly lots of examples):