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](https://arxiv.org/abs/1807.03423).
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.



Global to local principle for f.g. $\mathbb{Z}[x]$ modules
Your lemma easily follows from the [Smith Normal Form Theorem](https://en.wikipedia.org/wiki/Smith_normal_form), 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.
> 
> 
> 


