Increasing Mappings Satisfying Inclusion in Lower Closure is Isomorphic to Auxiliary Relations

From ProofWiki
Jump to: navigation, search

Theorem

Let $R = \left({S, \preceq}\right)$ be a bounded below join semilattice.

Let $\mathit{Ids}\left({R}\right)$ be the set of all ideals in $R$.

Let $L = \left({ \mathit{Ids}\left({R}\right), \precsim}\right)$ be an ordered set where $\precsim \mathop = \subseteq\restriction_{\mathit{Ids}\left({R}\right) \times \mathit{Ids}\left({R}\right)}$.

Let $M = \left({F, \preccurlyeq}\right)$ be the ordered set of increasing mappings $g:S \to \mathit{Ids}\left({R}\right)$ satisfying $\forall x \in S: g\left({x}\right) \subseteq x^\preceq$.

Let $\mathit{Aux}\left({R}\right)$ be the set of all auxiliary relations on $S$.

Let $P = \left({ \mathit{Aux}\left({R}\right), \precsim'}\right)$ be an ordered set where $\precsim' \mathop = \subseteq\restriction_{\mathit{Aux}\left({R}\right) \times \mathit{Aux}\left({R}\right)}$.


Then

there exists an order isomorphism between $P$ and $M$


Proof

By Segment of Auxiliary Relation Mapping is Element of Increasing Mappings Satisfying Inclusion in Lower Closure define $G:\mathit{Aux}\left({R}\right) \to F$

$\forall \mathcal R \in \mathit{Aux}\left({R}\right): G\left({\mathcal R}\right) = \left({S \ni x \mapsto x^{\mathcal R} }\right)$

We will prove by Order Isomorphism is Surjective Order Embedding that

$G$ is an order isomorphism.

Surjection

By Element of Increasing Mappings Satisfying Inclusion in Lower Closure is Generated by Auxiliary Relation:

$\forall f \in F: \exists \mathcal R \in \mathit{Aux}\left({R}\right): f = \left({S \ni x \mapsto x^{\mathcal R} }\right)$

By definition of image of mapping:

$\forall f \in F: f \in \operatorname{Im}\left({G}\right)$

Thus by definition:

$G$ is a surjection.

$\Box$

Order Embedding

Let $\mathcal R, \mathcal Q \in \mathit{Aux}\left({R}\right)$

We will prove that

$\mathcal R \precsim' \mathcal Q \implies G\left({\mathcal R}\right) \preccurlyeq G\left({\mathcal Q}\right)$

Let

$\mathcal R \precsim' \mathcal Q$

By definition of $\precsim'$:

$\mathcal R \subseteq \mathcal Q$

Let $x \in S$.

By Relation Segment is Increasing

$x^{\mathcal R} \subseteq x^{\mathcal Q}$

By Relation Segment of Auxiliary Relation is Ideal:

$x^{\mathcal R} \in \mathit{Ids}\left({R}\right)$ and $x^{\mathcal Q} \in \mathit{Ids}\left({R}\right)$

By definition of $\precsim$:

$x^{\mathcal R} \precsim x^{\mathcal Q}$

By definition of ordering on mappings:

$\left({S \ni x \mapsto x^{\mathcal R} }\right) \precsim \left({S \ni x \mapsto x^{\mathcal Q} }\right)$

Thus by definitions of $G$ and $\preccurlyeq$:

$G\left({\mathcal R}\right) \preccurlyeq G\left({\mathcal Q}\right)$

$\Box$


We will prove that

$G\left({\mathcal R}\right) \preccurlyeq G\left({\mathcal Q}\right) \implies \mathcal R \precsim' \mathcal Q$

Let

$G\left({\mathcal R}\right) \preccurlyeq G\left({\mathcal Q}\right)$

By definition of $G$ and $\preccurlyeq$:

$\left({S \ni x \mapsto x^{\mathcal R} }\right) \precsim \left({S \ni x \mapsto x^{\mathcal Q} }\right)$

Let $x, y \in S$ such that

$\left({x, y}\right) \in \mathcal R$

By definition of $\mathcal R$-segment:

$x \in y^{\mathcal R}$

By definition of ordering on mappings:

$y^{\mathcal R} \precsim y^{\mathcal Q}$

By definition of $\precsim$:

$y^{\mathcal R} \subseteq y^{\mathcal Q}$

By definition of subset:

$x \in y^{\mathcal Q}$

Thus by definition of $\mathcal Q$-segment:

$\left({x, y}\right) \in \mathcal Q$

By definition of subset:

$\mathcal R \subseteq \mathcal Q$

Thus by definition of $\precsim'$:

$\mathcal R \precsim' \mathcal Q$

$\blacksquare$

Sources