Finitely generated pp-types in saturated modules I'm working through Mike Prest's "Model Theory and Modules" and struggling a bit with one of the early exercises. Let $\mathcal{L}=\mathcal{L}_\text{ring}\cup\{r\}_{r\in R}$ be the language of right modules over a ring $R$, and fix a module $M$ in the language $\mathcal{L}$ and a subset $A\subseteq M$.
Recall that, to the stone space $S_n^M(A)$, there is the associated "positive primitive part" of $S_n^M(A)$, denoted $S_n^{+}(A)$, consisting of all pp-formulas in $S_n^M(A)$. Now, for any $p\in S_n^{+}(A)$, define $\mathcal{G}(p)=\{\varphi(v_1,...,v_n, \bar{0}):\varphi(\bar{v}, \bar{a})\in p\text{ for some }A\text{-tuple }\bar{a}\}$, and further define $G(p)=\bigcap_{\varphi\in\mathcal{G}(p)}\varphi(M^n,\bar{0})\leqslant M^n$. (A subgroup, though of course not necessarily a submodule if $R$ is not commutative.)
Finally, recall that a partial type $p(\bar{v})$ is "finitely generated" in $M$ if there is a formula $\varphi(\bar{v})$ (perhaps with parameters) such that $M\models \varphi(\bar{v})\rightarrow\psi(\bar{v})$ for any $\psi(\bar{v})\in p$. The exercise is then the following:

(i) Show that if $p\in S_n^{+}(A)$, $M$ is $|A|^+$-saturated, and $G(p)$ is pp-definable, then $p$ is finitely generated. Give an example to show that one needs some kind of saturation assumption on $M$.
(ii) Improve on (i) by showing that $|T|^+$-saturation is enough.

($T$ is not explicitly defined by Prest but presumably he is taking $T$ to be the complete $\mathcal{L}$-theory of $M$.) A counterexample without any saturation assumption is easy; for instance, consider $M=\mathbb{Z}$ as an abelian group, and let $p(v)$ be (the pp-part of a completion of the partial type consisting of $\{v\neq0\}$ unioned with) $\{\exists w (v=w n^k)\}_{k\in\mathbb{N}}$ for any $n>1$. Then $G(p)=\{0\}$, which is of course pp-definable, but $p(v)$ is clearly not finitely generated. I believe I've also shown the desired result in case that $M$ is $|A|^{+}$-saturated, but I'm unable to improve the bound. My solution is as follows (for simplicity I will restrict to the case where $p(v)$ is a 1-type):
Suppose $G(p)$ is cut out by a (pp-)formula $\theta(v)$. Now, define $C=\bigcap_{\varphi(v,\bar{a})\in p}\varphi(M,\bar{a})$. Each $\varphi(M,\bar{a})$ is a coset of $\varphi(M,\bar{0})$, so $C$ is either empty or a coset of $G(p)$. Since $M$ is $|A|^{+}$-saturated, and $p$ is a type with parameters from $A$, $p(v)$ is realized in $M$, so $C$ is non-empty, and thus it is a coset of $G(p)$; say $C=m+G(p)$ for some $m\in M$. Now clearly $C$ is (pp) definable over $\{m\}$, by the formula $\psi(v, m)=\exists w(\theta(w)\wedge v=w+m)$.
Now consider the set of formulas $\Sigma(v)=p(v)\cup\{\neg\psi(v, m)\}$. Certainly $\Sigma(v)$ is not realized in $M$, for by construction $M\models\psi(x, m)\iff x\in C\iff M\models p(x)$ for any $x\in M$. However, $\Sigma(v)$ is defined with parameters from $A\cup\{m\}$, a set with cardinality $<|A|^{+}$, and hence by the saturation assumption we must have that $\Sigma(v)$ is not (finitely) consistent with $M$.
Hence, taking conjunctions, there is a formula $\varphi(v, \bar{a})\in p(v)$ such that $M\models\forall v\neg(\varphi(v, \bar{a})\wedge\neg\psi(v, m))$, ie $M\models\forall v(\varphi(v, \bar{a})\rightarrow\psi(v, m))$, from which it is clear that $\varphi(v, \bar{a})$ generates $p(v)$, as desired. So this proves the problem when $M$ is $|A|^{+}$-saturated.
However, part (ii) seems very surprising to me, and I'm struggling to think of where to begin with it. Does anyone have any insight or hints?
Edit: Thanks to Alex Kruckman for pointing out a very silly mistake, now corrected.
 A: In fact maybe it's not so surprising... any two distinct cosets of a subgroup are of course disjoint, and so – because $p(v)$ is consistent – for any pp-formula $\varphi(v, \bar{0})$, there can be at most one coset of $\varphi(M, \bar{0})$ cut out by formulas of $p(v)$. Hence, removing duplicate formulas from $\Sigma(v)$ (ie formulas that cut out the same coset of a subgroup as another formula of $\Sigma(v)$), we obtain a new set of formulas $\Sigma'(v)$ over some set of parameters $A_0\cup\{m\}\subseteq A\cup\{m\}$ such that (i) $\Sigma'(v)$ and $\Sigma(v)$ are logically equivalent modulo $M$, and (ii) for any pp-formula $\varphi(v, \bar{0})$, $\varphi(v, \bar{a})$ appears in $\Sigma'(v)$ for at most one $A_0$-tuple $\bar{a}$. (We further remove from $A_0$ any elements not appearing in some formula of $\Sigma'(v)$.)
This condition (ii) guarantees that $|\Sigma'(v)|\leqslant |\{\text{pp-formulas over }\mathcal{L}\}|$. But now note, for any distinct pp-formulas $\varphi_1(v, \bar{0})$ and $\varphi_2(v, \bar{0})$ over $\mathcal{L}$, there are the distinct corresponding $\mathcal{L}$-sentences $\exists v \varphi_1(v, \bar{0})$ and $\exists v \varphi_2(v, \bar{0})$, and both are vacuously satisfied in $M$ (eg by $0$) and hence elements of $\text{Th}(M)$. So in fact we have $|\Sigma'(v)|\leqslant |\{\text{pp-formulas over }\mathcal{L}\}|\leqslant |\text{Th}(M)|$.
Finally, since only finitely elements of $A_0\cup\{m\}$ appear in any element of $\Sigma'(v)$, and every element of $A_0\cup\{m\}$ appears in at least one element of $\Sigma'(v)$, we have $|A_0\cup\{m\}|\leqslant \aleph_0 |\Sigma'(v)|\leqslant \aleph_0 |\text{Th}(M)|=|\text{Th}(M)|$, and so by considering $\Sigma'(v)$ instead $\Sigma(v)$ we need only $|\text{Th}(M)|^+$-saturation. Does this argument seem right?
