Ultraproduct is Well-Defined

Theorem

Definition:Ultraproduct is well-defined.

More specificly, following the definitions on Definition:Ultraproduct,

we are going to prove that:

(1) $f^\mathcal M$ is well-defined

(2) $R^\mathcal M$ is well-defined

Proof

First of all, we need to prove

Lemma

Following the definitions on Definition:Ultraproduct

$\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$, $k = 1, \dotsc, n$

if and only if

$\left\{ i : \left({m_{1, i}, \dots, m_{n, i} }\right) = \left({m'_{1, i}, \dots, m'_{n, i} }\right) \right \} \in \mathcal U$

Proof

Let

$I_k := \left\{ i \in I : m_{k, i} = m'_{k, i} \right\}$

$I^* := \left\{ i : \left({m_{1, i}, \dots, m_{n, i} }\right) = \left({m'_{1, i}, \dots, m'_{n, i} }\right) \right \}= \displaystyle \bigcap^n_{k = 1} I_k $

Suppose

$\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$ for $k = 1, \dotsc, n$

we have

$I_k \in \mathcal U$ for $k = 1, \dotsc, n$

Since $\mathcal U$ is closed under intersection

$I^* \in \mathcal U$

On the other hand, suppose

$I^* \in \mathcal U$

Since $\mathcal U$ is upward-closed

$I_k \in \mathcal U$ for $k = 1, \dotsc, n$

Therefore

$\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$

$\blacksquare$

Proposition 1

The definition of $f^\mathcal M$ is consistent.

i.e. for $\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$, $k = 1, \dotsc, n$

$\left(f^{\mathcal M_i}\left(m_{1, i}, \dots, m_{n, i}\right)\right)_\mathcal U = \left(f^{\mathcal M_i}\left(m'_{1, i}, \dots, m'_{n, i}\right)\right)_\mathcal U$

Proof

Firstly note that:

$\{i : f^{\mathcal M_i}\left(m_{1, i}, \dots, m_{n, i}\right) = f^{\mathcal M_i}\left(m'_{1, i}, \dots, m'_{n, i}\right) \} \supseteq \{i : \left(m_{1, i}, \dots, m_{n, i}\right) = \left(m'_{1, i}, \dots, m'_{n, i}\right) \} $

and by $\mathcal U$ is an ultrafilter on $I$, we have

$\{i : \left(m_{1, i}, \dots, m_{n, i}\right) = \left(m'_{1, i}, \dots, m'_{n, i}\right) \} \in \mathcal U$

implies

$\{i : f^{\mathcal M_i}\left(m_{1, i}, \dots, m_{n, i}\right) = f^{\mathcal M_i}\left(m'_{1, i}, \dots, m'_{n, i}\right) \} \in \mathcal U$

Therefore,

$\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$, $k = 1, \dotsc, n$, by #Lemma, which is equvalent to $\{i : \left(m_{1, i}, \dots, m_{n, i}\right) = \left(m'_{1, i}, \dots, m'_{n, i}\right) \} \in \mathcal U$

implies

$\left(f^{\mathcal M_i}\left(m_{1, i}, \dots, m_{n, i}\right)\right)_\mathcal U = \left(f^{\mathcal M_i}\left(m'_{1, i}, \dots, m'_{n, i}\right)\right)_\mathcal U$

$\blacksquare$

Proposition 2

The definition of $R^\mathcal M$ is consistent.

i.e. for $\left(m_{k, i}\right)_\mathcal U = \left(m'_{k, i}\right)_\mathcal U$, $k = 1, \dotsc, n$

$\left\{i \in I: \left({m_{1, i}, \dots, m_{n, i} }\right) \in R^\mathcal M_i\right\} \in \mathcal U$

if and only if

$\left\{i \in I: \left({m'_{1, i}, \dots, m'_{n, i} }\right) \in R^\mathcal M_i\right\} \in \mathcal U$

Proof

Let

$S := \left\{i \in I: \left({m_{1, i}, \dots, m_{n, i} }\right) \in R^\mathcal M_i\right\}$

$S' := \left\{i \in I: \left({m'_{1, i}, \dots, m'_{n, i} }\right) \in R^\mathcal M_i\right\}$

$I^* := \left\{ i : \left({m_{1, i}, \dots, m_{n, i} }\right) = \left({m'_{1, i}, \dots, m'_{n, i} }\right) \right \}$

$T := I^* \cap S$

$T' := I^* \cap S'$

As #Lemma implies

$I^* \in \mathcal U$

therefore

$S \in \mathcal U$ implies $T \in \mathcal U$

Note that

$\left({m_{1, i}, \dots, m_{n, i} }\right) = \left({m'_{1, i}, \dots, m'_{n, i} }\right)$ for $i \in I^*$

we have

$T = T'$

Hence

$T' \in \mathcal U$

and

$S' \in \mathcal U$ since $S' \supseteq T'$

So far we have proved

$S \in \mathcal U$ implies $S' \in \mathcal U$

By symmetry,

$S' \in \mathcal U$ implies $S \in \mathcal U$

$\blacksquare$