Elementary proof of "irreducible polynomials remain irreducible over transcendental extension"?

This may not be as elementary as you would like, but since you commented that it would be a step in the right direction, here is how you can replace the use of quantifier elimination with the Nullstellensatz.

Suppose that $K$ is algebraically closed, and that $F$ has a nontrivial factorization $F=GH$ over $L$. Let $A\subseteq L$ be the $K$-subalgebra generated by the coefficients of $G$ and $H$. Then $A$ is a finitely generated reduced commutative $K$-algebra. By the Nullstellensatz, for any nonzero $a\in A$, there exists a $K$-algebra homomorphism $\varphi:A\to K$ such that $\varphi(a)\neq 0$. In particular, pick nonzero coefficients of $G$ and $H$ other than the constant coefficients and let $a$ be their product, and let $\varphi:A\to K$ be such that $\varphi(a)\neq 0$.

Now, let $G'$ and $H'$ be the polynomials obtained by applying $\varphi$ to the coefficients of $G$ and $H$. Since $\varphi$ is a $K$-algebra homomorphism and $F$ has coefficients in $K$, we have $G'H'=F$. Moreover, since $\varphi(a)\neq 0$, $G'$ and $H'$ are both nonconstant. This contradicts the irreducibility of $F$.

(You can rephrase this to use more concrete version of the Nullstellensatz explicitly in terms of solving polynomial equations. Consider the equation $F=GH$ as a system of polynomial equations over $K$, with the variables being the coefficients of $G$ and $H$ and having one equation for each coefficient of $F$. By the Rabinowicz trick, you can add some more equations and variables that imply that $G$ and $H$ are nonconstant (pick a nonzero coefficient of each that is not the constant coefficient, and add a new variable which is its inverse). Since this system of equations has a solution in $L$, these polynomial equations cannot generate the unit ideal. By the weak Nullstellensatz, that implies they have a solution in $K$, which gives a factorization of $F$ over $K$.)


One way to see it is as follows: if $F$ is a field, $f_i = 0$ a system of polynomial equations with coefficients in $F$ that has finitely many solutions in any extension of $F$. Then any solution in an extension of $F$ has all components algebraic over $F$. Indeed, consider one solution in an extension $K$ of $F$. Let $F'$ the field generated by the components of that solution. It's enough to show that $F'$ is algebraic ( and so finite) over $F$. Indeed, if it were not, we would have infinitely many $F$ morphisms of $F'$ into some conveniently large extension $L$ of $F$. Each such morphism would produce a different solution of the system over $L$, contradiction.

Note that "finitely many solutions in any extension of $F$" is apriori stronger than "finitely many solutions in (some extension of )$\bar F$ ", although elimination of quantifiers clarifies they are equivalent statements. But we only use the weaker implication, that only uses basic field theory.

Now consider a factorization
$$P\cdot Q = R$$ where $R\in F[x_1, \ldots, x_n]$ and $P$, $Q \in K[x_1, \ldots, x_n]$. Let $I$, $J$ the largest monomials in the supports of $P$, $Q$ for some monomial order. Then for the coefficients $a_I$, $b_J$, $c_{I+J}$ of $P$, $Q$, $R$ we have $$a_I \cdot b_J = c_{I+J}$$ So let's choose a rescaling of the coefficients of $P$, $Q$ so that $$a_I = 1\\ b_J = c_{I+J}$$

Note that the system of equations for the coefficients of $P$, $Q$ ( polynomial, coefficients in $F$) that translates the equalities $$P\cdot Q = R\\ a_I= 1\\ b_J= c_{I+J}$$ has finitely many solutions in any extension $L$ of $F$ ( it follows from the fact that $L[x_1, \ldots,x_n]$ is UFD). We now conclude that the coefficients of $P$, $Q$ are algebraic over $F$.

The rescaling seems a bit unnatural. In fact one can show the following:

We have integral dependencies of any $a_I\cdot b_J$ over the ring $\mathbb{Z}[c_K]$. One can show this by induction on $n$, using Ex 8, 9 chap v in Atiyah-Macdonald Commutative Algebra. One can produce explicitely such dependencies for a given type of factorizations $P\cdot Q =R$, using Groebner bases for elimination.