\documentclass[12pt]{amsart}
\usepackage{amsmath, amsthm, amssymb, amsfonts}
\usepackage{enumerate}
\usepackage{verbatim}
%\numberwithin{equation}{section}

%%%Document Configuration
\pagestyle{headings}
%\addtolength{\topmargin}{-.5in}
\textwidth = 6in 
\oddsidemargin = .25in
\evensidemargin = .25in
\voffset = -1in
\textheight = 9.5 in
%\textwidth = 6in
%\parindent = 0in
%\headsep = 0in
\relpenalty = 9999
\binoppenalty = 9999
%linespacing
\renewcommand{\baselinestretch}{1.25}
\reversemarginpar     
%%%

%%%Theorem Configuration
\theoremstyle{plain}
\newtheorem*{main}{Main~Theorem}
\newtheorem{thm}{Theorem}[section]
\newtheorem*{thm*}{Theorem}
\newtheorem{cor}[thm]{Corollary}
\newtheorem{exer}[thm]{Exercise}
\newtheorem{fact}[thm]{Fact}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{remark}[thm]{Remark}
\newtheorem{hw}[section]{}
%\newtheorem{hw}[section]{HW}
\newtheorem{dfn}{Definition}[section]
\newtheorem*{dfn*}{Definition}
%%%

%%%Bibliography Configuration
\bibliographystyle{plain}
%%%

%%%semantic definitions
\DeclareMathOperator*{\Aut}{Aut}
\DeclareMathOperator*{\Dom}{Dom}
\DeclareMathOperator*{\Mod}{Mod}
\DeclareMathOperator*{\Th}{Th}
\DeclareMathOperator*{\tp}{tp}
\renewcommand{\div}{\mid}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\implies}{\Rightarrow}
\renewcommand{\natural}{\mathbb{N}}
\newcommand{\Acl}[1]{\obar{#1}}
\newcommand{\assign}{\leftarrow}
\newcommand{\caseif}{\Rightarrow}
\newcommand{\caseonlyif}{\Leftarrow}
\newcommand{\cantprove}{\nvdash}
\newcommand{\complex}{\mathbb{C}}
\newcommand{\field}{\mathbb{F}}
\newcommand{\minus}{\setminus}
\newcommand{\power}[1]{{\mathcal{P}}({#1})}
\newcommand{\nonnegative}{\mathbb{N}}
\newcommand{\integer}{\mathbb{Z}}
\newcommand{\intersect}{\cap}
\newcommand{\isomorphic}{\simeq}
\newcommand{\obar}[1]{\overline{#1}}
\newcommand{\proves}{\vdash}
\newcommand{\rational}{\mathbb{Q}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\union}{\cup}
\newcommand{\units}[1]{{\left(#1\right)}^{\times}}
%%%

%%%local definitions
\newcommand{\eleq}{\equiv}
\newcommand{\elleq}{\preccurlyeq}
\newcommand{\lang}[1]{{\mathcal{#1}}}
\newcommand{\Los}{{\L o\'s}}
\newcommand{\LS}{{L\"{o}wenheim-Skolem }}
\newcommand{\mathscr}[1]{{\mathcal{#1}}}
\newcommand{\monster}{{\mathbb{M}}}
\newcommand{\st}[1]{{\mathcal{#1}}}
\newcommand{\structure}[1]{{\mathcal{#1}}}
\newcommand{\struct}[1]{\left\langle#1\right\rangle}
\newcommand{\subst}{\prec}
\newcommand{\symAnd}{\mathop{\bigwedge}}
\newcommand{\symand}{\wedge}
\newcommand{\symimply}{\rightarrow}
\newcommand{\symiff}{\leftrightarrow}
\newcommand{\symnot}{\neg}
\newcommand{\symor}{\vee}
\newcommand{\tuple}[1]{\obar{#1}}
\newcommand{\Tfcp}{T_E^{\text{fcp}}}
\newcommand{\WFF}{well-formed formula}
\newcommand{\0}{\textbf{0}}
\newcommand{\suc}{\textbf{S}}
\newcommand{\A}{\mathfrak{A}}
\newcommand{\B}{\mathfrak{B}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\NNN}{\mathfrak{N}}
\newcommand{\E}{\textbf{E}}
\newcommand{\Cn}{\textrm{Cn}}
\newcommand{\res}{\upharpoonright}
%%%

\begin{document}

\title{Model Theory II Homework 11}
\author{Dakota Blair}
\maketitle

\setcounter{section}{21}

\begin{hw}
Prove that every ultrapower of a type $p$ over $M$ is an heir of $p$.
\end{hw}

\begin{proof}
Let $U$ be a nonprincipal ultrafilter on $I$
and $M^U$ and $p^U$
be the ultrapowers of $M$ and $p$ respectively.
Let $a$ be a realization in $p$ such that $a \in N$,
an elementary extension of $M$ with ultrapower $N^U$.
Let $g : M \to M^U$ and $f : N \to N^U$
denote the respective diagonal inclusion maps.
Given $\mu \in M^U$ denote by $\pi_i(\mu)$
the value of the $i$th coordinate of $\mu$.
Then
$\varphi(\tuple{x},\tuple{y}) \in p^U$
implies
$\exists b \in N$ such that $\varphi(\tuple{x}, \alpha) \in f(p)$.
This is true if and only if
there exists an $A \in U$ and a $\mu \in M^U$
such that $\forall i \in A$ we have $ M^U \models \varphi(\tuple{x}, f(\pi_i(\mu)))$
Thus
$\varphi(\tuple{x}, \mu) \in p^U \implies \varphi(\tuple{x}, \pi_i(\mu)) \in p$,
and
$\varphi(\tuple{x}, f(\pi_i(\mu))) \in p^U$
$N \models \varphi(a, \pi_i(\mu)) \implies N^U \models \varphi(f(a), f(\pi_i(\mu)))$
hence $\varphi(\tuple{x}, f(\pi_i(\mu))) \in f(p)$.
Therefore $p^U$ is an heir of $f(p)$.
\begin{comment}
Note to show $p^U = \tp(g(a)/N^U)$ is an heir of $f(p)$,

\[
(p)_M = \union_{m<\omega}
\{\varphi(\tuple{x},\tuple{y}) \in L_{n+m}
| \exists \tuple{a} \in A^m \text{ such that }
\varphi(\tuple{x},\tuple{a}) \in p\}
\]
$p^U$ is an heir of $p$ if $(p^U)_M = (p)_M$
\[
(p^U)_M = \union_{m<\omega}
\{\varphi(\tuple{x},\tuple{y}) \in L_{n+m}
| \exists \tuple{a} \in A^m \text{ such that }
\varphi(\tuple{x},\tuple{a}) \in p^U\}
\]
Let $\tuple{a}$ be some realization of $p$ in $N$ where $M \subst N$.
then $p^U = \tp((\tuple{a}^I/U)/M^U)$

$M \to M^U$
$\tuple{a} \mapsto \tuple{a}^U$
\end{comment}
\end{proof}

\begin{hw}
Prove $\tp(\tuple{a}/M\tuple{b})$ is an heir of $\tp(\tuple{a}/M)$
if and only if
$\tp(\tuple{b}/M\tuple{a})$ is an coheir of $\tp(\tuple{b}/M)$
\end{hw}

\begin{proof}
The type
$\tp(\tuple{a}/M\tuple{b})$ is an heir of $\tp(\tuple{a}/M)$
if and only if
for all $\varphi$ such that 
$\varphi(\tuple{x},\tuple{m},\tuple{b}) \in \tp(\tuple{a}/M\tuple{b})$
there is an $\tuple{m'} \in M$ such that
$\varphi(\tuple{x},\tuple{m},\tuple{m'}) \in \tp(\tuple{a}/M\tuple{b})$.
This is true if and only if, using dummy variables as necessary for the converse,
$\varphi(\tuple{a}, \tuple{m},\tuple{x}) \in \tp(\tuple{b}/M\tuple{a})
\implies \monster \models \varphi(\tuple{a}, \tuple{m}, \tuple{m'})$
which is true if and only if
$\tp(\tuple{b}/M\tuple{a})$ is an coheir of $\tp(\tuple{b}/M)$.
\end{proof}
\end{document}
