I am trying to prove the following theorem :
Let $T$ be some $L$-theory. Suppose that for any $n$, every type $p(\bar{x})\in S_n(T)$ is the only type extending $\{\varphi(\bar{x})\in p |\varphi(\bar{x})$ is quantifier free$\}$. Then $T$ has quantifier elimination.
I am trying to prove this in a topological way but got stuck at the end. Here is what I have done : I have $S_n(T)$ the space of complete types in $n$ variables (over $\emptyset$) w.r.t $T$, endowed with the topology where basis sets are of the form $[\varphi]=\{p(\bar{x})\in S_n(T)| \varphi \in p(\bar{x})$} where $\varphi(\bar{x})$ is a formula with $n$ free variables.
On the other hand I have $S_n^{qf}(T)$ , the space of maximal quantifier free types w.r.t $T$ endowed with the topology where basis sets are of the form $[\varphi]_{qf}=\{p(\bar{x})\in S_n^{qf}(T)| \varphi \in p(\bar{x})$} where $\varphi(\bar{x})$ is a QF formula with $n$ free variables.
I defined $f:S_n(T)\rightarrow S_n^{qf}(T)$ by $f(p)=\{\varphi(\bar{x})\in p |\varphi(\bar{x})$ is quantifier free$\}$. I proved $f$ is continuous and surjective. The assumption of the theorem gives us that $f$ is also injective. Since the spaces are compact and Hausdorff, $f$ is an homeomorphism.
Now I am a bit stuck. How the fact that $f$ is a homeomorphism helps me to prove that $T$ eliminates quantifiers ? I think I am in the right direction but don't know how to conclude.
Thank you !
I think the point you're missing is that in a Stone space, every clopen set is basic. This is part of Stone duality: you can recover a Boolean algebra from its Stone space as the algebra of clopen sets. But you can also prove it directly by compactness: Let $X$ be a clopen set. For every point $p\in X$, since $X$ is open there is a basic open set $[\varphi]$ with $p\in [\varphi]\subseteq X$. These basic opens form a cover of $X$, and since $X$ is closed, by compactness we can refine to a finite subcover, writing $X = \bigcup_{i = 1}^n [\varphi_i] = [\bigvee_{i=1}^n \varphi_i]$.
So suppose $\varphi$ is an arbitrary formula. Then $[\varphi]$ is clopen in $S_n(T)$, so $f([\varphi])$ is clopen in $S_n^{qf}(T)$, and thus $f([\varphi]) = [\psi]$ for some quantifier-free formula $\psi$. But then $[\varphi] = f^{-1}([\psi]) = [\psi]$ in $S_n(T)$, so $\varphi$ and $\psi$ are $T$-equivalent.