Faithful finite-step action of a Weyl algebra (source code)

= Faithful finite-step action of a Weyl algebra
{title2=$F_jA_n\hookrightarrow\operatorname{Hom}_\mathbb C(M_j,M_{2j})$}

For $M_j=F_jA_nM_0$ and $M_0\ne0$, the action map in the display is injective. If $a\in F_j$ kills $M_j$, each commutator $[a,z]$ with a generator lies in $F_{j-1}$ and kills $M_{j-1}$. Induction makes all these commutators zero, so $a$ is <scalar>; since it kills $M_0$, it is zero. This finite-step faithfulness does not require the whole <module> to be finite-dimensional.