Wanted: A purely algebraic proof of the Frobenius theorem on distributions

This answer is not correct as stated! See the comments below. The correct statement is more subtle. I will correct this eventually i hope.

Here's a (reasonably) algebraic proof of the Frobenius theorem (in the end there's a comment about the non-algebraic inputs of the proof):

Frobenius theorem: Let $M$ be an $n$-dimensional smooth manifold and let $D \subset TM$ be an involutive sub-bundle $[D,D] \subset D$ of rank $r$. Then $D$ is integrable

We first prove a slightly surprising lemma:

Lemma 1: Let $D \subset TM$ be as in the situation above. Then locally around any point $p\in M$ there's a local frame $\{X_1,...,X_r\} \subset \mathfrak{X}(U)$ for $D|_U$ with vanishing lie bracket $[X_i,X_j]=0$.

Proof:

Let $U$ be a small enough neighborhood of $p\in M$ s.t. both $\mathfrak{X}(U)$ and $\Gamma(U,D)$ are free as modules over $R:=C^{\infty}(U)$-modules.

Let $\{Y_1,...,Y_r\}$ and $\{\partial_1,...,\partial_n\}$ bases for $\Gamma(U,D)$ and $\mathfrak{X}(U)$ respectively. There's a unique matrix $A \in M_{r \times n}(R)$ satisfying:

$$ \left( \begin{matrix} Y_1 \\ \vdots \\ Y_r \\ \end{matrix} \right) = A \left( \begin{matrix} \partial_1 \\ \vdots \\ \partial_n \\ \end{matrix} \right) $$

The rank of $A$ must be $r$ and so up to relabeling of indices we may assume $A = (B|C)$ for some unique $B \in GL_r(R)$ and $C \in M_{r \times n-r}(R)$.

We define the frame $\{X_1,...,X_r\}$ by:

$$ \left( \begin{matrix} X_1 \\ \vdots \\ X_r \\ \end{matrix} \right) = B^{-1} \left( \begin{matrix} Y_1 \\ \vdots \\ Y_r \\ \end{matrix} \right) = B^{-1}A \left( \begin{matrix} \partial_1 \\ \vdots \\ \partial_n \\ \end{matrix} \right) $$

Since $B^{-1}A=(Id|B^{-1}C)$ we have $X_j = \partial_j+Z_j$ for some unique $Z_j \in Span \{\partial_{r+1},..., \partial_n\}$.

By the above we have $[X_i,X_j] \in Span \{\partial_{r+1},..., \partial_n\}$.

We recall now that $D$ is involutive so we also have $[X_i,X_j] \in Span \{X_1,...,X_r\}$.

But clearly the module $Span \{X_1,...,X_r\} / Span \{\partial_{r+1},..., \partial_n\} \cong Span \{\partial_1,...,\partial_r\}$ is free of rank $r$ and so we must have $Span \{X_1,...,X_r\} \cap Span \{\partial_{r+1},..., \partial_n\} = \{0\}$.

QED.

We actually proved something slightly stronger. Namely that for any involutive distribution $\mathcal{D} \subset \mathcal{T}_X$ there exists locally a retraction $\mathcal{T}_X|_U \to \mathcal{D}|_U$ and a local frame of commuting vector fields for $D|_U$ which preserve $\mathcal{I} = ker (\mathcal{T}_X|_U \to \mathcal{D}|_U)$ under the lie bracket.

Applying the theorem again to $\mathcal{I}$ we get locally a retraction $\mathcal{T}_X|_V \to \mathcal{I}|_V$ and a local frame for $\mathcal{I}|_V$ consisting of commuting vector fields preserving $ker(\mathcal{T}_X|_V \to \mathcal{I}|_V) \cong \mathcal{D}|_V$ under lie bracket. But since $\mathcal{D}|_V \cap \mathcal{I}|_V = \{0\}$ and both are involutive the frames for $\mathcal{D}|_V$ and $\mathcal{I}|_V$ must commute with each other.

We therefore have in fact proven the following very strong and surprising statement:

Theorem: Any involutive distribution $D$ is locally spanned by a frame of commuting vector fields which extends to a local frame for the entire tangent bundle also consisting of mutually commuting vector fields.

Proof of Frobenius theorem:

The dual frame in $\Omega^1_X$ of a commuting local frame for $TX$ consists entirely of closed 1-forms (this is a simple computation). By taking the dual of the frame in the theorem above we may apply Poincare's lemma to conclude that by sufficiently shrinking $U$ the basis of 1-forms can be lifted to a coordinate chart. A suitable projection will give the integrability of $D$.

QED.

The only non-algebraic statements in the proof are the Poincare lemma (a closed form is locally exact) and the existence of a locally commuting frame field (which is apparently true in the algebraic setting). A possible upshot of this is that the theorem generalizes immediately to the holomorphic case (by working everywhere with sheaves of modules over the sheaf of holomorphic functions and using the holomorphic poincare lemma).