[proofplan] We use the [Definability of Types in Stable Theories](/page/Definability%20of%20Types%20in%20Stable%20Theories) to choose a coherent $M$-[definitional scheme](/page/Definitional%20Scheme) for the [complete type](/page/Complete%20Type) $p$. The scheme is chosen compatibly with Boolean operations, so it decides every instance $\varphi(x;c)$ with $c$ from the monster model, and these decisions define a [global type](/page/Global%20Type) $\tilde q$. Coherence of the scheme gives completeness and finite consistency, while the fact that the defining predicates have parameters from $M$ gives $M$-[invariance](/page/Invariant%20Type). Finally, restricting $\tilde q$ to the parameter set $B = M \cup A$ gives the desired extension of $p$ over $B$. [/proofplan]

[step:Choose a coherent definitional scheme for the type over $M$] By the [Definability of Types in Stable Theories](/page/Definability%20of%20Types%20in%20Stable%20Theories), every [complete type](/page/Complete%20Type) over a model of a [stable theory](/page/Stable%20Theory) has a Boolean-compatible [definitional scheme](/page/Definitional%20Scheme) over that model. Since $T$ is stable, $M \models T$, and $p(x) \in S_x(M)$ is complete, we apply this result to $p$. For every formula $\varphi(x;y)$, choose an $M$-definable predicate $d_p\varphi(y)$ such that, for every $m \in M^{|y|}$, \begin{align*} \varphi(x;m) \in p \quad \iff \quad \mathfrak C \models d_p\varphi(m). \end{align*} The cited theorem supplies the scheme in coherent form: for all formulas $\varphi(x;y)$ and $\psi(x;z)$, the predicates satisfy the Boolean compatibility conditions \begin{align*} d_p(\neg \varphi)(y) &\leftrightarrow \neg d_p\varphi(y),\\ d_p(\varphi \wedge \psi)(y,z) &\leftrightarrow d_p\varphi(y) \wedge d_p\psi(z) \end{align*} in $\mathfrak C$. Equivalently, Boolean connectives in the $x$-variable are interpreted by the corresponding Boolean operations on the defining predicates in the parameter variables. The displayed binary conjunction compatibility extends to any finite conjunction $\bigwedge_{i=1}^{r} \varphi_i(x;y_i)$ by induction on $r$, with the case $r=1$ immediate and the induction step obtained by applying the binary compatibility to $\bigwedge_{i=1}^{r-1} \varphi_i(x;y_i)$ and $\varphi_r(x;y_r)$. This preserves the defining equivalence over $M$ because $p$ is complete and therefore decides negations and finite conjunctions exactly as a complete Boolean ultrafilter of formulas over $M$. [/step]

[step:Define a global type from the scheme and prove that it is complete and consistent]Define a set of formulas over $\mathfrak C$ by \begin{align*} \tilde q(x) := \{\,\varphi(x;c) : \varphi(x;y) \text{ is a formula},\ c \in \mathfrak C^{|y|},\ \mathfrak C \models d_p\varphi(c)\,\}. \end{align*} We first prove completeness. Let $\varphi(x;y)$ be a formula and let $c \in \mathfrak C^{|y|}$. By coherence, \begin{align*} d_p(\neg \varphi)(c) \leftrightarrow \neg d_p\varphi(c). \end{align*} Hence exactly one of $\mathfrak C \models d_p\varphi(c)$ and $\mathfrak C \models d_p(\neg\varphi)(c)$ holds. Therefore exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$ belongs to $\tilde q$. We next prove finite consistency. Let $\varphi_i(x;y_i)$ for $1 \le i \le r$ be formulas, let $c_i \in \mathfrak C^{|y_i|}$, and suppose $\varphi_i(x;c_i) \in \tilde q$ for each $i$. Define the conjunction formula \begin{align*} \theta(x;y_1,\dots,y_r) := \bigwedge_{i=1}^{r} \varphi_i(x;y_i). \end{align*} By coherence of the definitional scheme, \begin{align*} \mathfrak C \models d_p\theta(c_1,\dots,c_r). \end{align*} We claim that \begin{align*} \mathfrak C \models \exists x\,\theta(x;c_1,\dots,c_r). \end{align*} If not, then the $M$-definable formula \begin{align*} d_p\theta(y_1,\dots,y_r) \wedge \neg \exists x\,\theta(x;y_1,\dots,y_r) \end{align*} would be realized in $\mathfrak C$. Since $M \preceq \mathfrak C$ and all parameters occurring in $d_p\theta$ lie in $M$, elementarity gives tuples $m_i \in M^{|y_i|}$ such that \begin{align*} \mathfrak C \models d_p\theta(m_1,\dots,m_r) \wedge \neg \exists x\,\theta(x;m_1,\dots,m_r). \end{align*} The first conjunct implies $\theta(x;m_1,\dots,m_r) \in p$, by the defining property of $d_p\theta$ over $M$. Since $p$ is a complete type, every formula in $p$ is consistent with $T$ together with the elementary diagram of $M$, so \begin{align*} \mathfrak C \models \exists x\,\theta(x;m_1,\dots,m_r), \end{align*} contradicting the second conjunct. Thus every finite subset of $\tilde q$ is realized in $\mathfrak C$, so $\tilde q$ is consistent. By compactness, $\tilde q$ is consistent. Since the preceding completeness argument shows that $\tilde q$ decides every formula with parameters from $\mathfrak C$, this consistent set of formulas is a complete [global type](/page/Global%20Type) in $S_x(\mathfrak C)$.[/step]

[guided]We define the proposed global extension by letting the same formulas that define $p$ over $M$ decide instances over the whole monster model. For every formula $\varphi(x;y)$ and every parameter tuple $c \in \mathfrak C^{|y|}$, put \begin{align*} \varphi(x;c) \in \tilde q \quad \iff \quad \mathfrak C \models d_p\varphi(c). \end{align*} Equivalently, \begin{align*} \tilde q(x) = \{\,\varphi(x;c) : \varphi(x;y) \text{ is a formula},\ c \in \mathfrak C^{|y|},\ \mathfrak C \models d_p\varphi(c)\,\}. \end{align*} The first point to verify is completeness. Fix a formula $\varphi(x;y)$ and a tuple $c \in \mathfrak C^{|y|}$. A complete type must decide exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$. The coherence of the definitional scheme gives \begin{align*} d_p(\neg \varphi)(c) \leftrightarrow \neg d_p\varphi(c). \end{align*} Therefore exactly one of the two predicates $d_p\varphi(c)$ and $d_p(\neg\varphi)(c)$ holds in $\mathfrak C$. By the definition of $\tilde q$, exactly one of $\varphi(x;c)$ and $\neg\varphi(x;c)$ lies in $\tilde q$. The second point is finite consistency. Suppose \begin{align*} \varphi_1(x;c_1),\dots,\varphi_r(x;c_r) \end{align*} are finitely many formulas from $\tilde q$, where each $\varphi_i(x;y_i)$ is a formula and each $c_i \in \mathfrak C^{|y_i|}$. We must prove that these formulas can be realized simultaneously. Define the conjunction \begin{align*} \theta(x;y_1,\dots,y_r) := \bigwedge_{i=1}^{r} \varphi_i(x;y_i). \end{align*} Because each $\varphi_i(x;c_i)$ belongs to $\tilde q$, we have \begin{align*} \mathfrak C \models d_p\varphi_i(c_i) \end{align*} for every $1 \le i \le r$. Coherence of the definitional scheme turns the separate decisions into a decision for the conjunction: \begin{align*} \mathfrak C \models d_p\theta(c_1,\dots,c_r). \end{align*} Now we prove that the conjunction is realized. Suppose toward a contradiction that \begin{align*} \mathfrak C \models \neg \exists x\,\theta(x;c_1,\dots,c_r). \end{align*} Then the tuple $(c_1,\dots,c_r)$ realizes the $M$-definable condition \begin{align*} d_p\theta(y_1,\dots,y_r) \wedge \neg \exists x\,\theta(x;y_1,\dots,y_r). \end{align*} All parameters in $d_p\theta$ lie in $M$. Since $M \preceq \mathfrak C$, elementarity transfers the existence of such a tuple from $\mathfrak C$ down to $M$. Hence there are tuples $m_i \in M^{|y_i|}$ such that \begin{align*} \mathfrak C \models d_p\theta(m_1,\dots,m_r) \wedge \neg \exists x\,\theta(x;m_1,\dots,m_r). \end{align*} The first conjunct says, by the defining property of the scheme over $M$, that \begin{align*} \theta(x;m_1,\dots,m_r) \in p. \end{align*} But $p$ is a complete type over $M$, so every formula in $p$ is consistent with the elementary diagram of $M$. Therefore \begin{align*} \mathfrak C \models \exists x\,\theta(x;m_1,\dots,m_r), \end{align*} which contradicts the second conjunct. This proves that every finite subset of $\tilde q$ is satisfiable in $\mathfrak C$. By compactness, $\tilde q$ is consistent. Since we already proved that $\tilde q$ decides every formula with parameters from $\mathfrak C$, this consistent set of formulas is a complete global type over $\mathfrak C$.[/guided]

[step:Show that the global type extends $p$] Let $\varphi(x;y)$ be a formula and let $m \in M^{|y|}$. By the definition of $\tilde q$ and by the defining property of $d_p\varphi$ over $M$, \begin{align*} \varphi(x;m) \in \tilde q &\iff \mathfrak C \models d_p\varphi(m)\\ &\iff \varphi(x;m) \in p. \end{align*} Thus $\tilde q|_M = p$. [/step]

[step:Use $M$-definability to prove $M$-invariance]Let $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ be an automorphism fixing $M$ pointwise. Let $\varphi(x;y)$ be a formula and let $c \in \mathfrak C^{|y|}$. Since $d_p\varphi(y)$ is $M$-definable and $\sigma$ fixes every parameter from $M$, satisfaction of $d_p\varphi$ is preserved under $\sigma$: \begin{align*} \mathfrak C \models d_p\varphi(c) \quad \iff \quad \mathfrak C \models d_p\varphi(\sigma(c)). \end{align*} Using the definition of $\tilde q$ on both sides gives \begin{align*} \varphi(x;c) \in \tilde q \quad \iff \quad \varphi(x;\sigma(c)) \in \tilde q. \end{align*} Therefore $\tilde q$ is $M$-[invariant](/page/Invariant%20Type).[/step]

[guided]We prove invariance by checking the defining condition for an $M$-invariant type. Let $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ be an automorphism fixing every element of $M$, let $\varphi(x;y)$ be a formula, and let $c \in \mathfrak C^{|y|}$. The predicate $d_p\varphi(y)$ is $M$-definable, meaning that all parameters appearing in it are from $M$. Since $\sigma$ fixes those parameters pointwise, applying $\sigma$ preserves the truth of this predicate: \begin{align*} \mathfrak C \models d_p\varphi(c) \quad \iff \quad \mathfrak C \models d_p\varphi(\sigma(c)). \end{align*} Now translate both sides back into membership in $\tilde q$ using the definition of the global type. The left side is equivalent to $\varphi(x;c) \in \tilde q$, and the right side is equivalent to $\varphi(x;\sigma(c)) \in \tilde q$. Thus \begin{align*} \varphi(x;c) \in \tilde q \quad \iff \quad \varphi(x;\sigma(c)) \in \tilde q. \end{align*} This is exactly invariance under automorphisms fixing $M$, so $\tilde q$ is $M$-[invariant](/page/Invariant%20Type).[/guided]

[step:Restrict the global type to $B = M \cup A$]Define \begin{align*} q := \tilde q|_B. \end{align*} Since $\tilde q \in S_x(\mathfrak C)$ is complete, its restriction to the parameter set $B$ is a complete type in $S_x(B)$. Since $M \subseteq B$ and $\tilde q|_M = p$, we have \begin{align*} q|_M = (\tilde q|_B)|_M = \tilde q|_M = p. \end{align*} Thus $q$ extends $p$. The type $q$ inherits its intended invariance through the global type $\tilde q$: if $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ and $c \in B^{|y|}$ with $\sigma(c) \in B^{|y|}$, then \begin{align*} \varphi(x;c) \in q &\iff \varphi(x;c) \in \tilde q\\ &\iff \varphi(x;\sigma(c)) \in \tilde q\\ &\iff \varphi(x;\sigma(c)) \in q. \end{align*} This proves that $q$ is the restriction to $B$ of the [global type](/page/Global%20Type) $\tilde q$, which is $M$-[invariant](/page/Invariant%20Type) and was built from the $M$-[definitional scheme](/page/Definitional%20Scheme) for $p$.[/step]

[guided]The theorem asks for a type over the smaller parameter set $B = M \cup A$, not necessarily for the whole global type. We therefore define \begin{align*} q := \tilde q|_B. \end{align*} Because $\tilde q$ is a complete type over $\mathfrak C$, its restriction to formulas with parameters from $B$ is a complete type over $B$, so $q \in S_x(B)$. Since $M \subseteq B$, restricting first to $B$ and then to $M$ gives the same result as restricting directly to $M$: \begin{align*} q|_M = (\tilde q|_B)|_M = \tilde q|_M = p. \end{align*} Thus $q$ is an extension of $p$ from $M$ to $B$. Finally, the promised invariance is inherited from the global type rather than proved as an independent property of an arbitrary type over $B$. If $\sigma \in \operatorname{Aut}(\mathfrak C/M)$ and $c \in B^{|y|}$ with $\sigma(c) \in B^{|y|}$, then membership in $q$ is the same as membership in $\tilde q$ for formulas whose parameters are in $B$. Therefore \begin{align*} \varphi(x;c) \in q &\iff \varphi(x;c) \in \tilde q\\ &\iff \varphi(x;\sigma(c)) \in \tilde q\\ &\iff \varphi(x;\sigma(c)) \in q. \end{align*} The middle equivalence is exactly the $M$-invariance of $\tilde q$ proved above. Hence $q$ is the restriction to $B$ of a global $M$-[invariant](/page/Invariant%20Type) type constructed from the $M$-[definitional scheme](/page/Definitional%20Scheme) for $p$, which is the conclusion of the theorem.[/guided]