Good filtration for the order filtration (source code)

= Good filtration for the order filtration
{title2=$M_j=\sum_{\ell=1}^sF_{j-d_\ell}A_n\,m_\ell$}

= Good filtrations for the order filtration
{synonym}

For the <order filtration of a Weyl algebra>, a <filtration of a module> is good if it is increasing, exhaustive, zero in sufficiently negative degrees, compatible with multiplication, and has <associated graded module> finite over the <associated graded ring>. Equivalently it has the displayed finite shifted-generating description. Choose homogeneous generators of the <associated graded module>, lift them to $m_\ell$, and successively remove the top symbol of any element; the lower bound on the <filtration of a module> makes this process terminate. Conversely, the displayed description makes the symbols of the $m_\ell$ generate. Each $M_j$ is finite over the degree-zero <polynomial ring> $\mathbb C[x_1,\ldots,x_n]$; it need not be a <finite-dimensional vector space> over $\mathbb C$.