I have the following setup, I expect that it is studied in the theory of $D$-modules, and I apologize in advance if I am wrong.
First, I have an algebra $A$ of differential operators on $n$ variables with coefficients being rational functions of the variables (I'm mostly interested in $n=2$). There is also a right $A$-linear map $$\phi: A\times \ldots \times A\to A\times \ldots \times A$$ ($k$ factors on the left, $l$ factors on the right), which basically describes a system of $l$ first order differential equations on $k$ functions. I.e. if $f_j$ are the arguments of $\phi$ and $g_i$ are the components of $\phi$, then $$ g_i=\sum_j a_{ij} f_j, $$ where $a_{ij}$ are first-order differential operators. The system of equations is then $g_i=0$.
Now, $M=\ker \phi$ is a right $A$-module, and I am interested in its properties. Of course, it should significantly depend on $\phi$. I do not want to give a concrete description of $\phi$ as it is rather complicated, and it is not clear to me for which properties of it I should be looking.
Rather, I know from brute force calculation that in my examples $M$ is free, and its rank is equal to the number "of functional degrees of freedom" of the solutions to the system of equations corresponding to $\phi$. By the latter I mean that if I choose one of the $n$ variables as time $t$, and treat the system as describing temporal evolution, then the time derivatives of $\mathrm{rk}\, M$ unknown functions are not fixed by the system. In the same interpretation, there are some constraints on purely "space" derivatives of unknown functions, but these "commute" with the evolution equations and it is sufficient to satisfy them for initial data.
How can one approach proving that $M$ is free? Namely, are there some general results, which guarantee this, given some conditions on $\phi$? Are there, perhaps, some keywords I should look for, or is there a rephrasing of this setup which is more common in mathematics literature?
I think that I can prove that $M$ is finitely-generated, and construct an overcomplete generating set (for explicit expressions I need computer help). It is possible that one can use it to prove freeness by brute force starting from the construction, but before trying this, I was wondering if there is a more general approach.
