Global to local principle for f.g. $\mathbb{Z}[x]$ modules In graduate school, while I was working on the maximal subgroup growth of certain metabelian groups, I discovered and proved a lemma which gave me the impression that it was already known. Do you know of any reference for this result? Does it follow easily from a known result?  Here is the result: 
Let $N$ be a finitely generated $\mathbb{Z}[x]$-module. 
Suppose (by using the fundamental theorem of f.g. modules over PIDs) we have the following isomorphism of $\mathbb{Q}[x]$-modules:
$$\mathbb{Q} \otimes_\mathbb{Z} N \cong \left( \bigoplus_{j=1}^{s_1} \mathbb{Q}[x]/(a_j) \right) \oplus \mathbb{Q}[x]^{s_2} $$
for some $a_j \in \mathbb{Q}[x]$ that are not units and such that $a_1 \mid a_2 \mid \ldots \mid a_{s_1}$.
Then for all large primes $p$, we have the following isomorphism of $\mathbb{F}_p[x]$-modules:
$$N/pN \cong \left( \bigoplus_{j=1}^{s_1} \mathbb{F}_p[x]/(\overline{a_j}) \right) \oplus \mathbb{F}_p[x]^{s_2}.$$

While my proof of the above result is about three pages long, I do have a short heuristic argument:
When doing the computation required in finding the decomposition of $\mathbb{Q} \otimes N$ into a direct sum of cyclic modules, the only thing keeping us from doing this computation to $N$ itself (as a $\mathbb{Z}[x]$-module) is that we may need to divide by finitely many integers. 
So if $p$ is large enough, then in $\mathbb{F}_p$ we can divide by all those integers (i.e. their residues mod $p$). For such $p$,  the steps of the algorithm would be the same for $N/pN$ as for $\mathbb{Q} \otimes N$.

In case you are interested, this is Lemma 41 in my arXiv paper
Maximal subgroup growth of some metabelian groups.
I actually proved a slight generalization, concerning finitely generated $D^{-1}\mathbb{Z}[x]$-modules, where $D$ is the multiplicative closure of a finite set of primes.
 A: Your lemma easily follows from the Smith Normal Form Theorem, a result you already referred to. The short heuristic argument that you gave can indeed be turned into a short proof.
Nothing in the sequel should be new to you. But it is shorter and it also makes clear that your lemma generalizes immediately when replacing $\mathbb{Z}$ by any integral domain with infinitely many maximal ideals ("for all prime $p$ large enough" becomes "for all but finitely many maximal ideals").
Given a rational prime number $p$, let $\mathbb{Z}_{(p)} = \left\{ \frac{r}{s} \, \vert \, r, s \in \mathbb{Z},\, \mathbb{Z}s + \mathbb{Z}p = \mathbb{Z} \right\}$ and let $\phi_p: \mathbb{Z}_{(p)} \rightarrow \mathbb{Z}_{(p)} / p\mathbb{Z}_{(p)} \simeq \mathbb{F}_p$ be the natural epimorphism. Restricted to $\mathbb{Z}$, the map $\phi_p$ is the reduction modulo $p$. Given a commutative and unital ring $R$, we denote by $\text{M}_{m,n}(R)$ the $R$-module of the $m$-by-$n$ matrices over $R$.
Abusing notation, we denote also by $\phi_p$ the epimorphisms
$
\mathbb{Z}_{(p)}[x] \rightarrow \mathbb{F}_p[x]$ and $\text{M}_{m,n}(\mathbb{Z}_{(p)}[x]) \rightarrow \text{M}_{m,n}(\mathbb{F}_p[x])
$
induced by the reduction of coefficients.

Proof of OP's Lemma. Let $N$ be a finitely generated module over $\mathbb{Z}[x]$ and let 
  \begin{equation} \label{EqSeq}
\mathbb{Z}[x]^n \xrightarrow[]{f} \mathbb{Z}[x]^m \rightarrow N \rightarrow 0 \quad\quad (1)
\end{equation} 
   be an exact sequence that provides us with a presentation of $N$ where $m$ is the minimal number of generators of $N$. Let $M(f) \in \text{M}_{m, n}(\mathbb{Z}[x])$ be the matrix of $f$ with respect to the canonical bases. Applying the tensor functors $-\otimes_{\mathbb{Z}[x]} \mathbb{Q}[x]$ and $-\otimes_{\mathbb{Z}[x]} \mathbb{F}_p[x]$ to $(1)$, we obtain two other exact sequences. The exactness of the first is immediate as $-\otimes_{\mathbb{Z}[x]} \mathbb{Q}[x]$ is exact since we just inverted non-zero rational integers. For the second, some easy diagram chasing involving also $(1)$ settles the claim. Thus we get a presentation of $N \otimes_{\mathbb{Z}[x]}\mathbb{Q}[x]$ as the cokernel of the matrix $M(f\otimes_{\mathbb{Z}[x]}\mathbb{Q}[x]) = M(f)$ and a presentation of $N \otimes_{\mathbb{Z}[x]}\mathbb{F}_p[x] \simeq N/pN$ as the cokernel of  $M(f\otimes_{\mathbb{Z}[x]}\mathbb{F}_p[x]) = \phi_p(M(f)) \in \text{M}_{m,n}(\mathbb{F}_p[x]))$.
  Since $\mathbb{Q}[x]$ is a principal ideal ring, the Smith Normal Form Theorem applies. Therefore we can find $A \in \text{GL}_m(\mathbb{Q}[x]), B \in \text{GL}_n(\mathbb{Q}[x])$ such that 
  $$AM(f)B = \text{diag}(a_1, \dots, a_{s_1}, \underbrace{0, \dots, 0}_{s_2 \text{ zeroes}}) \quad (2)$$ with $a_j \in \mathbb{Q}[x]$ for all $j$, $a_j \vert a_{j + 1}$ and $a_1 \notin \mathbb{Q} \setminus \{0\}$. For all $p$ sufficiently large, we have $A \in \text{GL}_m(\mathbb{Z}_{(p)}[x]), B \in \text{GL}_n(\mathbb{Z}_{(p)}[x])$ and hence $a_j \in \mathbb{Z}_{(p)}[x]$ for all $j$. Applying $\phi_p$ to both sides of $(2)$, we get $$\phi_p(A) \phi_p(M(f)) \phi_p(B) = \text{diag}(\phi_p(a_1), \dots, \phi_p(a_{s_1}), 0, \dots, 0).$$ The proof is then complete.

