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$?



Constructive proof of "Projective implies proper"
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.


