Up-Complete Product

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\left({S, \preceq_1}\right)$, $\left({T, \preceq_2}\right)$ be non-empty ordered sets.

Let $\left({S \times T, \preceq}\right)$ be Cartesian product of $\left({S, \preceq_1}\right)$ and $\left({T, \preceq_2}\right)$.


Then

$\left({S \times T, \preceq}\right)$ is up-complete if and only if both $\left({S, \preceq_1}\right)$ and $\left({T, \preceq_2}\right)$ are also up-complete.

Lemma 1

Let $X$ be a directed subset of $S$.

Let $Y$ be a directed subset of $T$.

Then $X \times Y$ is also a directed subset of $S \times T$.


Lemma 2

Let $X$ be a directed subset of $S \times T$.

Then

$\operatorname{pr}_1^\to\left({X}\right)$ and $\operatorname{pr}_2^\to\left({X}\right)$ are directed

where

$\operatorname{pr}_1$ denotes the first projection on $S \times T$
$\operatorname{pr}_2$ denotes the second projection on $S \times T$
$\operatorname{pr}_1^\to\left({X}\right)$ denotes the image of $X$ under $\operatorname{pr}_1$


Proof

Sufficient Condition

Assume that

$\left({S \times T, \preceq}\right)$ is up-complete.

Let $X$ be a directed subset of $S$.

By assumption:

$T \ne \varnothing$

By definition by non-empty set:

$\exists t: t \in T$

By Singleton is Directed and Filtered Subset:

$\left\{ {t}\right\}$ is directed

By Lemma 1:

$X \times \left\{ {t}\right\}$ is a directed subset of $S \times T$

By definition of up-complete:

$X \times \left\{ {t}\right\}$ admits a supremum

By definition of supremum:

$\exists \left({a, b}\right) \in S \times T: \left({a, b}\right)$ is upper bound for $X \times \left\{ {t}\right\}$ and
$\forall \left({c, d}\right) \in S \times T: \left({c, d}\right)$ is upper bound for $X \times \left\{ {t}\right\} \implies \left({a, b}\right) \preceq \left({c, d}\right)$

We will prove that

$a$ is upper bound for $X$

Let $s \in X$.

By definition of Cartesian product:

$\left({s, t}\right) \in X \times \left\{ {t}\right\}$

By definition of upper bound:

$\left({s, t}\right) \preceq \left({a, b}\right)$

Thus by definition of Cartesian product of ordered sets:

$s \preceq_1 a$


We will prove that

$\forall x \in S: x$ is upper bound for $X \implies a \preceq_1 x$

Let $x \in S$ such that

$x$ is upper bound for $X$

We will prove as sublemma that

$\left({x, b}\right)$ is upper bound for $X \times \left\{ {t}\right\}$

Let $\left({y, z}\right) \in X \times \left\{ {t}\right\}$.

By definition of Cartesian product:

$y \in X$

By definition of upper bound:

$\left({y, z}\right) \preceq \left({a ,b}\right)$

By definition of Cartesian product of ordered sets:

$z \preceq_2 b$

By definition of upper bound:

$y \preceq_1 x$

Thus by definition of Cartesian product of ordered sets:

$\left({y, z}\right) \preceq \left({x, b}\right)$

This ends the proof of sublemma.

Then:

$\left({a, b}\right) \preceq \left({x, b}\right)$

Thus by definition of Cartesian product of ordered sets:

$x \preceq_1 a$


Thus by definition of supremum:

$X$ admits a supremum:

Thus by definition

$\left({S, \preceq_1}\right)$ is up-complete

By mutatis mutandis

$\left({T, \preceq_2}\right)$ is up-complete


Necessary Condition

Assume that

$\left({S, \preceq_1}\right)$ and $\left({T, \preceq_2}\right)$ are up-complete.

Let $X$ be directed subset of $S \times T$.

By Lemma 2

$\operatorname{pr}_1^\to\left({X}\right)$ and $\operatorname{pr}_2^\to\left({X}\right)$ are directed

where

$\operatorname{pr}_1$ denotes the first projection on $S \times T$
$\operatorname{pr}_2$ denotes the second projection on $S \times T$

By definition of up-complete:

$\operatorname{pr}_1^\to\left({X}\right)$ and $\operatorname{pr}_2^\to\left({X}\right)$ admit suprema

By definition of supremum:

$\exists a \in S: a$ is upper bound for $\operatorname{pr}_1^\to\left({X}\right)$ and
$\forall c \in S: c$ is upper bound for $\operatorname{pr}_1^\to\left({X}\right) \implies a \preceq_1 c$

and

$\exists b \in T: b$ is upper bound for $\operatorname{pr}_2^\to\left({X}\right)$ and
$\forall c \in T: c$ is upper bound for $\operatorname{pr}_2^\to\left({X}\right) \implies b \preceq_2 c$

We will prove that

$\left({a, b}\right)$ is upper bound for $X$

Let $\left({x, y}\right) \in X$.

By definitions of image of set and projections:

$x \in \operatorname{pr}_1^\to\left({X}\right)$ and $y \in \operatorname{pr}_2^\to\left({X}\right)$

By definition of upper bound:

$x \preceq_1 a$ and $y \preceq_2 b$

Thus by definition of Cartesian product of ordered sets:

$\left({x, y}\right) \preceq \left({a, b}\right)$


We will prove that

$\forall \left({x, y}\right) \in S \times T: \left({x, y}\right)$ is upper bound for $X \implies \left({a, b}\right) \preceq \left({x, y}\right)$

Let $\left({x, y}\right) \in S \times T$ such that

$\left({x, y}\right)$ is upper bound for $X$

We will prove as sublemma that

$x$ is upper bound for $\operatorname{pr}_1^\to\left({X}\right)$

Let $c \in \operatorname{pr}_1^\to\left({X}\right)$.

By definitions of image of set and projections:

$\exists d: \left({c, d}\right) \in X$

By definition of upper bound:

$\left({c, d}\right) \preceq \left({x, y}\right)$

Thus by definition of Cartesian product of ordered sets:

$c \preceq_1 x$


By mutatis mutandis

$y$ is upper bound for $\operatorname{pr}_2^\to\left({X}\right)$

Then:

$a \preceq_1 x$ and $b \preceq_2 y$

Thus by definition of Cartesian product of ordered sets:

$\left({a, b}\right) \preceq \left({x, y}\right)$

By definition

$X$ admits a supremum.

Thus by definition

$\left({S \times T, \preceq}\right)$ is up-complete.

$\blacksquare$


Sources