Constructive proof of "Projective implies proper"

Question

For every ring $A$, the structural morphism of schemes $\pi_A : {\bf P}^n_{A} \to {\rm Spec}{A}$ is a closed map. The usual proof of this fact is not constructive : given equations of a closed subset $Z$ of ${\bf P}^n_{A}$, it doesn't produce equations for $\pi_A(Z)$.

In the case $A$ is a polynomial ring over an algebraically closed field $k$, this result is none other than the fundamental theorem of elimination theory : the image of a Zariski-closed subset of ${\bf P}^n(k) \times k^m$ under the second projection is a Zariski-closed subset of $k^m$. The first proofs of this theorem (Cayley, Kronecker, Sylvester) used resultants and thus were constructive.

In fact, the proof using elimination theory is universal in the following sense. Given integers $n,r \geq 1$, $d_1,\ldots,d_r \geq 1$, consider the universal homogenous polynomials $P_1,\ldots,P_r$ of degree $d_1,\ldots,d_r$ in the indeterminates $T_0,\ldots,T_n$, having coefficients in the polynomial ring $\widetilde{A} = \mathbf{Z}[Y_{i,\alpha} : 1 \leq i \leq r]$, where the indeterminates $Y_{i,\alpha}$ are the coefficients of $P_i$. Then there exists an explicit "resultant system" $R_1,\ldots,R_s \in \widetilde{A}$ such that $\pi_{\widetilde{A}}(V_+(P_1,\ldots,P_r))=V(R_1,\ldots,R_s)$. This means that specializations of $P_1,\ldots,P_r$ in some algebraically closed field $k$ have a common root in ${\bf P}^n(k)$ if and only if the corresponding specializations of $R_1,\ldots,R_s$ all vanish. Of course $s$ has to depend on $n,r,d_i$, but everything is explicit (at least from a theoretical point of view).

Now let $A$ be any ring and let $I=(f_1,\ldots,f_r)$ be an homogenous ideal of finite type of $A[T_0,\ldots,T_n]$. Then the resultant system above specialized at $f_1,\ldots,f_r$ provides explicit equations for $\pi_A(V_+(I))$ (this can be seen by studying the geometric fibers of $\pi_A$). In particular if $A$ is noetherian, then the map $\pi_A$ is closed, and we have a constructive proof for that. But in general, a closed subset of ${\bf P}^n_A$ need not be defined by finitely many equations. This raises the following questions :

1. Is there a way to prove that the map $\pi_A$ is closed for every ring $A$, by some clever reduction to the noetherian case?

2. If $Z$ is a closed subset of ${\bf P}^n_A$, given to us by infinitely many explicit equations $(f_i)_{i \in I}$, is there a way to produce explicit equations for $\pi_A(Z)$? In other words, is there a constructive proof of the fact that $\pi_A$ is closed?

3. Regarding question 2, an obvious thing to do is to look at all finite subfamilies $(f_i)_{i \in J}$, where $J$ is a finite subset of $I$, and to consider the associated resultant systems. Are all these equations sufficient to define $\pi_A(Z)$?

EDIT. Will Sawin has proved that the answers to all these questions is yes. Following Daniel Litt's comment, we can also consider $\pi_A(Z)$ as a closed subscheme of $\operatorname{Spec} A$, namely the closed subscheme defined by the kernel of the morphism $A \to \mathcal{O}_Z(Z)$. Do the resultant systems generate this ideal of $A$?

Answer 1

3, and thus 2 and 1: yes. By checking equality between the two sets at each point, we reduce to the case where the base is a point. But points are always Noetherian schemes, and the statement is obviously true for Noetherian schemes.

Edit: I was just reminded of this question and I realize that I now know the answer. If an element is in the kernel of the morphism $A \to \mathcal O_Z(Z)$, then it is in the kernel of the map to $\mathcal O_Z$ restricted to each of the $n+1$ standard affine open sets in $\mathbb P^n_A$. In each of those sets, it is in the ideal generated by the $f_i$. Of course if you are in the ideal generated by the $f_i$ then you are in the ideal generated by finitely many of them. Taking a finite union over the $n+1$ different affine opens, we get a finite set of relations that proves this element is in the kernel. So finite elimination theory generates infinite elimination theory.