Finite modules with a connection on a complex polynomial open are vector bundles

Fix $p$ and write $A=R_{{\mathfrak{m}}_p}$, $\mathfrak{m}={\mathfrak{m}}_{p}A$, $V=N_p$. Choose lifts $v_1,\dots ,v_r$ of a basis of $V\mathrm{/}\mathfrak{m}V$. The quotient $Q=V\mathrm{/}\sum A{v}_i$ is finite and satisfies $\mathfrak{m}Q=Q$. By [F1], $(1-a)Q=0$ for some $a\in \mathfrak{m}$. Since $1-a$ is a unit, $Q=0$, so the lifts generate $V$. For $r=0$ this proves $V=0$.

Suppose ${\sum }_i{a}_i{v}_i=0$ is a nonzero relation. Fiber independence gives $a_i\in \mathfrak{m}$. Let $k$ be the least order of vanishing at $p$ of a nonzero $a_i$. This is finite: a nonzero rational regular germ is a quotient of polynomials with nonzero denominator at $p$, so its convergent Taylor series has a first nonzero coefficient. Choose a multi-index $\beta$ of order $k$ with some ${\mathrm{\partial }}^{\beta }{a}_i(p)\mathrm{\ne }0$. Apply the ordered connection derivatives prescribed by $\beta$ to the relation. By repeated Leibniz, every term in which a derivative hits $v_i$ has fewer than $k$ derivatives on its coefficient and vanishes modulo $\mathfrak{m}$. Reduction therefore gives ${\sum }_i{\mathrm{\partial }}^{\beta }{a}_i(p){\bar{v}}_i=0$, contradicting the fiber basis. Hence there are no relations, and $V$ is free.

The local basis extends to a principal algebraic neighborhood. Lift its finitely many elements through denominators to sections on some neighborhood of $p$. Their cokernel and the kernel of the resulting finite free presentation are finite by [F2]. Since their localizations at $p$ vanish, each finite generating set is killed after inverting a single element nonzero at $p$; multiply these finitely many elements. On the resulting smaller principal neighborhood the map is an isomorphism. The case $n=0$ is the finite-dimensional vector-space assertion over $\mathbb{C}$ and the same proof is valid.

A stable submodule and its quotient are finite by [F2] and inherit Leibniz operators; the proof just given applies to both without a category-O assumption. Commutators descend if initially zero. A surjection onto a locally free module splits locally by lifting a finite basis, so a short exact sequence gives an exact fiber sequence. This proves every assertion.