The Tarski-Seidenberg Theorem states that the polynomial image of a semi-algebraic set is semi-algebraic. A semi-algebraic subset of a Euclidean space $\Bbb{R}^n$ is by definition a finite union of subsets of the form 
$$
\{P\_1=\dots=P\_k=0, Q\_1>0,\dots,Q\_l>0\}
$$
where $P\_i$'s and $Q\_j$'s belong to $\Bbb{R}[x\_1,\dots,x\_n]$. I wonder is there a general coordinate-free version of this theorem for morphisms of real varieties? (By a real variety I mean the set of $\Bbb{R}$-points of a variety over $\Bbb{R}$.) 



General Tarski-Seidenberg Theorem
The most abstract version of the Tarski-Seidenberg theorem I know of is the following



> 
> Let $f:A\to B$ be a morphism of finite presentation of commutative rings. Then the induced map
> 
> 
> $$f^\*:\operatorname{Sper}B\to \operatorname{Sper}A$$
> 
> 
> sends constructible sets to constructible sets.
> 
> 
> 


Here $\operatorname{Sper}$ is the [*real spectrum*](https://mathoverflow.net/a/344859/) of the ring, i.e. the set of all pairs $(p,<)$ where $p$ is a prime ideal and $<$ is an order on the residue field at $p$.


It is well known (e.g. theorem 7.2.3 in Bochnack-Coste-Roy *Real Algebraic Geometry*) that if $A$ is an algebra of finite presentation over $\mathbb{R}$, the boolean algebra of constructible subsets of $\operatorname{Sper}A$ is in natural bijection with the semialgebraic subsets of the real points of the variety $\operatorname{Spec}A$.


