# Stable group acting on a type definable set.

We work inside a saturated $$M \models T$$ with $$T$$ $$\omega$$-stable. We may even assume $$T = \mathsf{ACF}$$.

Let $$G$$ be a connected definable group together with a transitive definable action of $$G$$ over a type definable set $$Y$$. Then $$Y$$ is definable.

I am thinking of proving it by using $$Y = G \cdot y$$ for any $$y \in Y$$, and somehow using compactness and definability of $$(G, \cdot)$$, but I need to find some $$y \in Y$$ such that $$\{ y \}$$ is definable (I believe). Something else I wanted to use is the descending chain condition for stable groups, and writing $$Y = \bigcap_i \phi_i(M)$$ for some set of formulas, and then somehow go back to $$G$$ to prove $$Y = \phi_{i_1}(M) \cap \dots \cap \phi_{i_n}(M)$$, using transitivity in the process. I am however, unable to put these together or see intuitively why $$Y$$ should be definable.

Any help is appreciated.

Your idea to define $$Y$$ as $$G\cdot b$$ for some $$b\in Y$$ is a good one. In general, there's no reason why there should be a definable element of $$Y$$. But why use one element of $$Y$$ when you can use them all? By which I mean: instead of using an arbitrary parameter, use the "canonical parameter" in $$M^{\text{eq}}$$.
Proof 1: Let $$\varphi(x,y)$$ be the formula expressing $$x\in G\cdot y$$. Let $$E$$ be the equivalence relation defined by $$yEy'\iff \forall x\, (\varphi(x,y)\leftrightarrow \varphi(x,y'))$$. Since the action of $$G$$ on $$Y$$ is transitive, for any $$b\in Y$$, $$Y = [b]_E$$. Since $$Y$$ is type-definable, $$Y$$ is fixed by all automorphisms, so the element $$[b]_E$$ in $$M^{\text{eq}}$$ is fixed by all automorphisms. Thus, $$[b]_E$$ is a definable element, and hence $$Y$$ is a definable set.
Essentially the same argument gives the following more general (and fundamental) result: Suppose $$A\subseteq B$$ and $$Y$$ is definable over $$B$$ and $$A$$-invariant (fixed setwise by all automorphisms that fix $$A$$ pointwise). Then $$Y$$ is definable over $$A$$.
Proof 2: Let $$\Phi(y)$$ be the partial type defining $$Y$$. Since the action of $$G$$ on $$Y$$ is transitive, the following partial type is inconsistent: $$\Phi(y)\cup \Phi(y')\cup \{\lnot (\exists x\in G\, x\cdot y = y')\}$$. By compactness, there is some formula $$\varphi(y)$$ which is a finite conjunction of formulas in $$\Phi(y)$$, such that $$\varphi(y)\land \varphi(y')\land \lnot (\exists x\in G\, x\cdot y = y')$$ is inconsistent. Let $$Y'$$ be the set defined by $$\varphi(y)$$. The $$Y\subseteq Y'$$, and the action of $$G$$ on $$Y'$$ is transitive, so $$Y = Y'$$.