Up-Complete Product
Theorem
Let $\struct {S, \preceq_1}$, $\struct {T, \preceq_2}$ be non-empty ordered sets.
Let $\struct {S \times T, \preceq}$ be the simple order product of $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$.
Then:
- $\struct {S \times T, \preceq}$ is up-complete if and only if both $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ are also up-complete.
Proof
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$.
$\Box$
Lemma 2
Let $X$ be a directed subset of $S \times T$.
Then
- $\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ are directed
where
- $\pr_1$ denotes the first projection on $S \times T$
- $\pr_2$ denotes the second projection on $S \times T$
- $\map {\pr_1^\to} X$ denotes the image of $X$ under $\pr_1$
$\Box$
Sufficient Condition
Assume that:
- $\struct {S \times T, \preceq}$ is up-complete.
Let $X$ be a directed subset of $S$.
By assumption:
- $T \ne \O$
By definition by non-empty set:
- $\exists t: t \in T$
By Singleton is Directed and Filtered Subset:
- $\set t$ is directed
By Lemma 1:
- $X \times \set t$ is a directed subset of $S \times T$
By definition of up-complete:
- $X \times \set t$ admits a supremum
By definition of supremum:
- $\exists \tuple {a, b} \in S \times T: \tuple {a, b}$ is upper bound for $X \times \set t$
and:
- $\forall \tuple {c, d} \in S \times T: \tuple {c, d}$ is upper bound for $X \times \set t \implies \tuple {a, b} \preceq \tuple {c, d}$
We will prove that
- $a$ is upper bound for $X$
Let $s \in X$.
By definition of Cartesian product:
- $\tuple {s, t} \in X \times \set t$
By definition of upper bound:
- $\tuple {s, t} \preceq \tuple {a, b}$
Thus by definition of simple order product:
- $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:
- $\tuple {x, b}$ is upper bound for $X \times \set t$
Let $\tuple {y, z} \in X \times \set t$.
By definition of Cartesian product:
- $y \in X$
By definition of upper bound:
- $\tuple {y, z} \preceq \tuple {a, b}$
By definition of simple order product:
- $z \preceq_2 b$
By definition of upper bound:
- $y \preceq_1 x$
Thus by definition of simple order product:
- $\tuple {y, z} \preceq \tuple {x, b}$
This ends the proof of sublemma.
$\Box$
Then:
- $\tuple {a, b} \preceq \tuple {x, b}$
Thus by definition of simple order product:
- $x \preceq_1 a$
Thus by definition of supremum:
- $X$ admits a supremum:
Thus by definition:
- $\struct {S, \preceq_1}$ is up-complete.
- $\struct {T, \preceq_2}$ is up-complete
Necessary Condition
Assume that
- $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ are up-complete.
Let $X$ be directed subset of $S \times T$.
By Lemma 2:
- $\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ are directed
where
- $\pr_1$ denotes the first projection on $S \times T$
- $\pr_2$ denotes the second projection on $S \times T$
By definition of up-complete:
- $\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ admit suprema
By definition of supremum:
- $\exists a \in S: a$ is upper bound for $\map {\pr_1^\to} X$
and:
- $\forall c \in S: c$ is upper bound for $\map {\pr_1^\to} X \implies a \preceq_1 c$
and
- $\exists b \in T: b$ is upper bound for $\map {\pr_2^\to} X$
and:
- $\forall c \in T: c$ is upper bound for $\map {\pr_2^\to} X \implies b \preceq_2 c$
We will prove that
- $\tuple {a, b}$ is upper bound for $X$
Let $\tuple {x, y} \in X$.
By definitions of image of set and projections:
- $x \in \map {\pr_1^\to} X$ and $y \in \map {\pr_2^\to} X$
By definition of upper bound:
- $x \preceq_1 a$ and $y \preceq_2 b$
Thus by definition of simple order product:
- $\tuple {x, y} \preceq \tuple {a, b}$
We will prove that
- $\forall \tuple {x, y} \in S \times T: \tuple {x, y}$ is upper bound for $X \implies \tuple {a, b} \preceq \tuple {x, y}$
Let $\tuple {x, y} \in S \times T$ such that:
- $\tuple {x, y}$ is upper bound for $X$
We will prove as sublemma that
- $x$ is upper bound for $\map {\pr_1^\to} X$
Let $c \in \map {\pr_1^\to} X$.
By definitions of image of set and projections:
- $\exists d: \tuple {c, d} \in X$
By definition of upper bound:
- $\tuple {c, d} \preceq \tuple {x, y}$
Thus by definition of simple order product:
- $c \preceq_1 x$
- $y$ is upper bound for $\map {\pr_2^\to} X$
Then:
- $a \preceq_1 x$ and $b \preceq_2 y$
Thus by definition of simple order product:
- $\tuple {a, b} \preceq \tuple {x, y}$
By definition
- $X$ admits a supremum.
Thus by definition
- $\struct {S \times T, \preceq}$ is up-complete.
$\blacksquare$
Sources
- 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices
- Mizar article WAYBEL_2:funcreg 3
- Mizar article WAYBEL_2:11