Supremum of Meet Image of Directed Set

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \preceq}$ be an up-complete meet semilattice.

Let $f: S \times S \to S$ be a mapping such that:

$\forall \tuple {x, y} \in S \times S: \map f {x, y} = x \wedge y$

Let $D$ be directed subset of $S \times S$ in the simple order product $\struct {S \times S, \precsim}$ of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.

Then:

$\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$

where

$\pr_1$ denotes the first projection on $S \times S$
$\pr_2$ denotes the second projection on $S \times S$
$\map {\pr_1^\to} D$ denotes the image of $D$ under $\pr_1$.


Proof

By definition of image of set:

$\map {f^\to} D = \set {x \wedge y: \tuple {x, y} \in D}$

By definition of subset:

$\map {f^\to} D \subseteq \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$

By Up-Complete Product/Lemma 2:

$D_1 := \map {\pr_1^\to} D$ is directed

and

$D_2 := \map {\pr_2^\to} D$ is directed.

By Meet of Directed Subsets is Directed:

$\set {x \wedge y: x \in D_1, y \in D_2}$ is directed.

By definition of up-complete:

$\set {x \wedge y: x \in D_1, y \in D_2}$ admits a supremum.

By Meet is Increasing:

$f$ is increasing mapping.

By Image of Directed Subset under Increasing Mapping is Directed:

$\map {f^\to} D$ is directed.

By definition of up-complete:

$\map {f^\to} D$ admits a supremum.

By Supremum of Subset:

$\map \sup {\map {f^\to} D} \preceq \sup \set {x \wedge y: x \in D_1, y \in D_2}$

We will prove that

$\set {x \wedge y: x \in D_1, y \in D_2} \subseteq \paren {\map {f^\to} D}^\preceq$

where

$\paren {\map {f^\to} D}^\preceq$ denotes the lower closure of $\map {f^\to} D$.

Let $z \in \set {x \wedge y: x \in D_1, y \in D_2}$.

Then

$\exists x \in D_1, y \in D_2: z = x \wedge y$

By definition of image of set:

$\exists \tuple {a, b} \in D: \map {\pr_1} {a, b} = x$

and

$\exists \tuple {c, d} \in D: \map {\pr_2} {c, d} = y$:

By definition of first projection and second projection:

$a = x$ and $d = y$

By definition of directed subset:

$\exists \tuple {g, h} \in D: \tuple {x, b} \precsim \tuple {g, h} \land \tuple {c, y} \precsim \tuple {g, h}$

By definition of simple order product:

$x \preceq g$ and $y \preceq h$

By Meet Semilattice is Ordered Structure:

$x \wedge y \preceq g \wedge h \in \set {x \wedge y: \tuple {x, y} \in D}$

Thus by definition of lower closure:

$z \in \paren {\map {f^\to} D}^\preceq$

$\Box$


By Supremum of Lower Closure of Set:

$\paren {\map {f^\to} D}^\preceq$ admits a supremum

and

$\map \sup {\map {f^\to} D}^\preceq = \map \sup {\map {f^\to} D}$

By Supremum of Subset:

$\sup \set {x \wedge y: x \in D_1, y \in D_2} \preceq \map \sup {\map {f^\to} D}$

Thus by definition of antisymmetry:

$\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in D_1, y \in D_2}$

$\blacksquare$


Sources