What a joke to think that I could live without the internet.
Recall that the Frobenius Theorem is actually quite a concise statement given what we’ve defined and done. It just says that every involutive distribution is completely integrable.
Let D be involutive of dimension k and M an n-manifold and . We need a flat chart about p. We will work on a coordinate chart since it is a local property, and hence with loss of generality we replace the manifold with an open subset of Euclidean space. Suppose is a smooth local frame for D. We choose our coordinates such that is complementary to the span of .
Now let be the projection onto the first k coordinates. Then we get a bundle morphism . Explicitly this is just .
The morphism is smooth, since it is composition of the inclusion map from the distribution followed by . Thus, by definition, the component functions in any smooth frame are smooth. In particular, we have smooth frames and . Thus the matrix entries of with respect to these frames are smooth functions of q.
We also get that at any given point p, this restricted map is bijective as a map to . It is certainly surjective by construction, and when restricted is complementary to the kernel of the non-restricted bundle map by choice of coordinates. Thus it is bijective in an entire neighborhood of p. Thus we have a smooth inverse in this neighborhood .
Define a frame for D on this neighborhood by . Note that if we can show that we will be done. This is because the frame will be a commuting frame, and the “canonical form” for a commuting frame is precisely our definition of a flat chart.
We have that . i.e. we have that and are -related.
But now we have it by naturality of the Lie bracket, since . And the involutivity of D tells us that is in D, and since on the distribution is injective, for every point in the neighborhood.