Am struggling a bit with a step of the model theoretic proof of the Nullstellensatz. The proof essentially runs as follows: Take $I\subset J\subset K[x_1, ..., x_n]$ radical ideals of some algebraically closed field $k$, and let $f\in J\setminus I$. By a simple lemma we may find a prime ideal $P\subset K[x_1, ..., x_n]$ containing $I$ but not $f$. Then $K[x_1, ..., x_n]/P$ is an integral domain, so let $L$ be the algebraic closure of its fraction field. Then, if $f_1, ..., f_m$ generate $I$, and $\phi$ is the sentence expressing that there exists $(y_1, ..., y_n)$ a mutual root of $f_1, ..., f_m$ and not a root of $f$, $L\models \phi$ (seen by taking $y_i=x_i/P\in L)$. Now, so the argument runs, by model-completeness of the theory of algebraically closed fields we must also have $K\models \phi$, and so there exists some element of $K^n$ that is a root of $f_1, ..., f_n$ but not $f$. Hence $V(J)\neq V(I)$ and so we are done.
Almost all of this is clear to me; the one thing that's tripping me up is in the application of the model-completeness of ACF. In particular, we have to show that there an embedding of $K$ into $L$ for the result to apply, and this isn't entirely obvious to me. Will someone tell me if the following argument is correct? :
Of course $K$ can be interpreted as the constant subfield of $K[x_1, ..., x_n]$, and so can we identify each $r\in K$ with the coset $r/P\in L$. The only necessary thing is to show injectivity of this identification; if $P$ does not contain a unit, then injectivity is clear. If $P$ does contain a unit, then $P=K[x_1, ..., x_n]$, a contradiction as we supposed that $f\notin P$.
Yes, that's correct. Note that it's not even meaningful to say $L\models\phi$ until you have chosen an embedding $K\to L$, since the polynomials $f_i$ and $f$ have coefficients in $K$ (not $L$!) and so we need a way to consider them as polynomials over $L$. Likewise, it is important that we choose the specific embedding $K\to L$ that you describe, since otherwise we wouldn't know that $L\models \phi$ is actually true: when we interpret $\phi$ in $L$, it says there exists a root in $L$ of the $f_i$ that is not a root of $f$ when we use our chosen embedding $K\to L$ to evaluate these polynomials on elements of $L$, and we only know that is true of the elements $y_i=x_i/P$ if we use the "obvious" embedding $K\to L$ rather than some different one.