Ultraproduct is Well-Defined
If you are fairly certain that there are none, please remove {{proofread}} from the code.
Please fix formatting and $\LaTeX$ errors and inconsistencies.
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Theorem
Ultraproduct is well-defined.
Proof
Specifically, following the definitions on ultraproduct, it is to be proved that:
- $(1) \quad f^\MM$ is well-defined
- $(2) \quad R^\MM$ is well-defined
First of all, we need to prove:
Lemma
Following the definitions on ultraproduct:
- $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$, $k = 1, \dotsc, n$
- $\set {i \in I: \tuple {m_{1, i}, \dots, m_{n, i} } = \tuple {m'_{1, i}, \dots, m'_{n, i} } } \in \UU$
Proof
Let:
| \(\ds I_k\) | \(:=\) | \(\ds \set {i \in I: m_{k, i} = m'_{k, i} }\) | ||||||||||||
| \(\ds I^*\) | \(:=\) | \(\ds \set {i \in I: \tuple {m_{1, i}, \dots, m_{n, i} } = \tuple {m'_{1, i}, \dots, m'_{n, i} } } = \bigcap^n_{k = 1} I_k\) |
Suppose:
- $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$ for $k = 1, \dotsc, n$
We have:
- $I_k \in \UU$ for $k = 1, \dotsc, n$
Since $\UU$ is closed under intersection:
- $I^* \in \UU$
On the other hand, suppose:
- $I^* \in \UU$
Since $\UU$ is upward-closed:
- $I_k \in \UU$ for $k = 1, \dotsc, n$
Therefore:
- $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$
$\blacksquare$
Proposition 1
The definition of $f^\MM$ is consistent.
that is, for $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$, $k = 1, \dotsc, n$
- $\eqclass {\map {f^{\MM_i} } {m_{1, i}, \dotsc, m_{n, i} } } \UU = \eqclass {\map {f^{\MM_i} } {m'_{1, i}, \dotsc, m'_{n, i} } } \UU$
Proof
Firstly note that:
- $\set {i \in I: \map {f^{\MM_i} } {m_{1, i}, \dotsc, m_{n, i} } = \map {f^{\MM_i} } {m'_{1, i}, \dots, m'_{n, i} } } \supseteq \set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } = \tuple {m'_{1, i}, \dotsc, m'_{n, i} } }$
and by $\UU$ is an ultrafilter on $I$:
- $\set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } = \tuple {m'_{1, i}, \dotsc, m'_{n, i} } } \in \UU$
implies:
- $\set {i \in I: \map {f^{\MM_i} } {m_{1, i}, \dotsc, m_{n, i} } = \map {f^{\MM_i} } {m'_{1, i}, \dotsc, m'_{n, i} } } \in \UU$
Therefore:
- $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$, $k = 1, \dotsc, n$
by the lemma, which is equvalent to:
- $\set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } = \tuple {m'_{1, i}, \dotsc, m'_{n, i} } } \in \UU$
implies:
- $\eqclass {\map {f^{\MM_i} } {m_{1, i}, \dotsc, m_{n, i} } } \UU = \eqclass {\map {f^{\MM_i} } {m'_{1, i}, \dotsc, m'_{n, i} } } \UU$
$\blacksquare$
Proposition 2
The definition of $R^\MM$ is consistent.
that is, for $\eqclass {m_{k, i} } \UU = \eqclass {m'_{k, i} } \UU$, $k = 1, \dotsc, n$:
- $\set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } \in R^{\MM_i} } \in \UU$
- $\set {i \in I: \tuple {m'_{1, i}, \dotsc, m'_{n, i} } \in R^{\MM_i} } \in \UU$
Proof
Let:
| \(\ds S\) | \(:=\) | \(\ds \set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } \in R^{\MM_i} }\) | ||||||||||||
| \(\ds S'\) | \(:=\) | \(\ds \set {i \in I: \tuple {m'_{1, i}, \dotsc, m'_{n, i} } \in R^{\MM_i} }\) | ||||||||||||
| \(\ds I^*\) | \(:=\) | \(\ds \set {i \in I: \tuple {m_{1, i}, \dotsc, m_{n, i} } = \tuple {m'_{1, i}, \dots, m'_{n, i} } }\) | ||||||||||||
| \(\ds T\) | \(:=\) | \(\ds I^* \cap S\) | ||||||||||||
| \(\ds T'\) | \(:=\) | \(\ds I^* \cap S'\) |
From the lemma:
- $I^* \in \UU$
therefore:
- $S \in \UU \implies T \in \UU$
Note that:
- $\tuple {m_{1, i}, \dots, m_{n, i} } = \tuple {m'_{1, i}, \dotsc, m'_{n, i} }$ for $i \in I^*$
we have:
- $T = T'$
Hence:
- $T' \in \UU$
and:
- $S' \in \UU$ since $S' \supseteq T'$
So far we have proved:
- $S \in \UU \implies S' \in \UU$
By symmetry:
- $S' \in \UU \implies S \in \UU$
$\blacksquare$