I am trying to figure out what are the isolated 1-types an algebraically closed field $K$, with parameters taken from a subfield $k\subseteq K$, and am almost done except for deciding on one specific 1-type (corresponding to the generic point in the Zariski topology).
The context is that in chapter 4 of Marker's book on Model Theory, it was proven that $S_n(k)$ coincides with Spec$k[x_1,..,x_n]$ by a continuous bijection $p\mapsto \{f(x)\in k[x]:f(x_1,...,x_n)=0)\in p\}$, i.e by taking those polynomials that define zero inequalities in the type.
Now the closed points $J$ of Spec$k[x]$ correspond to Galois orbits of the algebraic closure of $k$, and thus all such $J$ must come from types of elements of $K$ algebraic over $k$. I proved in a previous exercise of Marker's book that types of algebraic elements are isolated.
Question 1: However, with the generic point $(0)$ of Spec$k[x]$, I am not sure. I suspect it is not isolated. So far, I concluded that if $p$ is the corresponding type of $(0)$ then for every nonzero polynomial $f(x)\in k[x]$, the un-equation $f(x)\neq0$ must lie in $p$. This implies $p$ cannot be isolated by a conjunction of polynomial un-equations. I'm not sure how to show formulas of other shapes cannot isolate $p$.
Quesiton 2: (note): Thank you Levon, it turns the proof that the isolated types are correspond precisely to the closed points to the above only required a small note. Now this leads me to wonder in general, i.e. in in higher dimensions, using Marker's identification of $S_n(k)$, are the isolated types exactly those corresponding to closed points of the Zariski topology?
To continue your line of approach, you can assume $\phi(x) \in p$ isolates the generic type. By quantifier elimination $\phi(x)$ can be taken to be quantifier free. Next put it in the disjunctive normal form, say $\phi(x) = \bigvee_{i = 1, ..., n} \psi_i(x)$. Then for some $i$, we get that $\psi_i(x) \in p$. And so it also isolates the generic type. But $\psi_i$ has to be a conjunction of polynomial un-equations.
However, the easiest way to see that the generic type is not isolated is to observe that it can be omitted in the model $acl(k)$.