Does the main theorem of elimination theory with $\mathbb{Z}$-coefficients imply that projective varieties are complete? I have a question concerning the completeness of projective varieties.
Let $k$ be an algebraically closed field. By the "main theorem of elimination theory" I mean the following result:
Let $f_1,\ldots,f_r\in\mathbb{Z}[X_0,\ldots,X_n,Y_1,\ldots,Y_m]$ be homogeneous in $X_0,\ldots,X_n$. Then there exist polynomials $g_1,\ldots,g_s\in \mathbb{Z}[Y_1,\ldots,Y_n]$ such that for all $a\in k^m$ the system $f_1(X,a)=\cdots=f_r(X,a)=0$ has a nontrivial solution in $k$ if and only if $g_1(a)=\cdots=g_s(a)=0.$
I want to deduce that projective varieties over $k$ are complete. Since closed subvarieties of complete varieties are complete and every variety is a finite union of open affines, it suffices to prove that the projection $\mathbb{P}^n(k)\times \mathbb{A}^m(k)\to \mathbb{A}^m(k)$ to the second factor is closed. The above "main theorem of elimination theory" gives us that the image of a closed set defined by polynomials with integer coefficients is closed. Does it already follow somehow that the image of a closed set defined by polynomials with coefficients in $k$ is closed?
Context: In Exercise 3.4.22 of Marker's "Model Theory. An Introduction", part (a) asks for a nice model theoretic proof of the "main theorem" as stated above. The task in part (b) is to deduce that projective varieties are complete.
Thanks for your help!
Edit: Thanks for your answers! I have come up with this "elementary" solution, giving a little more details to the proof in the comment by Alex Kruckman. Please let me know when I did a mistake.
For the general case, now let $f_1,\ldots,f_r\in k[X_0,\ldots,X_n,Y_1,\ldots,Y_m]$ be homogeneous in the $X_0,\ldots,X_n$ and let $Z$ be their vanishing set in $\mathbb{P}^n(k)\times\mathbb{A}^m(k)$. We want to show that $\mathrm{pr}_2(Z)$ is closed in $\mathbb{A}^m(k)$. Let $(\mu_i)_{i=1}^N$ be the finitely many coefficients of $f_1,\ldots,f_r$. replacing each $\mu_i$ by a new variable $W_i$, we obtain polynomials
\begin{align*}
\tilde f_1,\ldots,\tilde f_r\in \mathbb{Z}[X_0,\ldots,X_n,Y_1,\ldots,Y_m,W_1,\ldots,W_N]
\end{align*}
that are homogeneous in the $X_0,\ldots,X_n$. Let $\tilde Z$ denote their vanishing set in $\mathbb{P}^n(k)\times\mathbb{A}^{m+N}(k)$. Consider the commutative diagram

where the vertical maps $p$ and $p'$ are also the obvious projection maps. By the statement for $\mathbb{Z}$-coefficients, the map $\mathrm{pr}_2\times\mathrm{id}$ is closed. The projection $p$ restricts to an isomorphism from the closed set $\tilde Z\cap V((W_i-\mu_i)_{i=1}^N)$ to $Y$ and we have
\begin{align*}
(\mathrm{pr}_2\times\mathrm{id})(\tilde Z\cap V((W_i-\mu_i)_{i=1}^N))=(\mathrm{pr}_2\times\mathrm{id})(\tilde Z)\cap  V((W_i-\mu_i)_{i=1}^N),
\end{align*}
which is closed because $(\mathrm{pr}_2\times\mathrm{id})(\tilde Z)$ is closed. We observe that $p'$ restricts to an isomorphism from $(\mathrm{pr}_2\times\mathrm{id})(\tilde Z)\cap  V((W_i-\mu_i)_{i=1}^N)$ to $\mathrm{pr}_2(Y)$, and we conclude that $\mathrm{pr}_2(Y)$ is closed.
 A: One way to reduce completeness of projective space to $\mathbb{Z}$ is to use noetherian approximation techniques from scheme theory.
Def: Let $R$ be a ring. We say a $R$-scheme $X$ is universally closed if for every $R$-scheme $T$, the projection $X \times_R T \to T$ is closed in the Zariski topology.
It is not hard to see that it suffices to check the statement only on affine schemes $T = \mathrm{Spec}\ A$. Using the observation that $X \times_R T = (X \times_R R') \times_{R'} T$ for any ring homomorphism $R \to R'$ and $R'$-scheme $T$, we see that if $X/R$ is universally closed, then so is $X \times_R R'/R'$. The key approximation result is the following which is proved in Tag 05JW of the Stacks Project.
Lemma: Let $X/R$ be quasi-compact. Then $X$ is universally closed if and only if the projection $X \times \mathbb{A}^m \to \mathbb{A}^m_R$ is closed.
The hard part of the proof is to show that if $X/R$ is not universally closed, then there exists some finitely presented affine scheme $T$ such that $X \times_R T \to T$ is not closed. Since every finitely presented affine scheme $T$ embeds as a closed subscheme of $\mathbb{A}^m_R$ for some $m$, the reverse implication follows.
Prop: For any ring $R$, $\mathbb{P}^n_R$ is universally closed.
Proof. By the observation above, it suffices to show the claim for $R = \mathbb{Z}$. By the lemma, it suffices to show that the morphism of $\mathbb{Z}$-schemes $\pi : \mathbb{P}^n \times \mathbb{A}^m \to \mathbb{A}^m$ is closed in the Zariski topology. Every closed subscheme $Z \subset \mathbb{P}^n \times \mathbb{A}^m$ is given by the vanishing of $f_1, \ldots, f_r$ as in the hypothesis of the Main Theorem of Elimination Theory. Let $W \subset \mathbb{A}^m$ be the closed subscheme defined as the vanishing of $g_1, \ldots, g_s$. Then the projection of $Z$ is $W$ and thus $\pi$ is closed. Indeed every point $p \in Z$ is the image of some $k$-point $\bar{p} : \mathrm{Spec}\ k \to Z$ where $k$ is an algebraically closed field. Thus $\pi(p)$ is the image of $\pi \circ \bar{p} \in \mathbb{A}^m(k)$ which lies in $W(k)$ by the Main Theorem.
I think this argument, and in particular the key lemma above can be rephrased in a way that only makes reference to $k$-points. Namely one can try to show that any closed subvariety of $X(k) \times \mathbb{A}^m(k)$ which witnesses the failure of the projection to be closed is defined over some finitely generated ring extension $R/\mathbb{Z}$, and by writing $R = \mathbb{Z}[a_1, \ldots, a_s]/I$, produces a closed subvariety of $X(k) \times \mathbb{A}^{m+s}(k)$ defined over $\mathbb{Z}$ whose image under projection is not closed. While I was writing this answer Alex Kruckman suggested essentially this argument in the comments. I think there is something to be gained by thinking about schemes though so I'll leave the scheme theoretic argument too.
