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

Theorem

Let $R = \struct {S, \preceq}$ be a bounded below join semilattice.

Let $\map {\operatorname{Ids} } R$ be the set of all ideals in $R$.

Let $L = \struct {\map {\operatorname{Ids} } R, \precsim}$ be an ordered set where $\precsim \mathop = \subseteq\restriction_{\map {\operatorname{Ids} } R \times \map {\operatorname{Ids} } R}$.

Let $M = \struct {F, \preccurlyeq}$ be the ordered set of increasing mappings $g:S \to \map {\operatorname{Ids} } R$ satisfying $\forall x \in S: \map g x \subseteq x^\preceq$.

Let $\map {\operatorname{Aux} } R$ be the set of all auxiliary relations on $S$.

Let $P = \struct {\map {\operatorname{Aux} } R, \precsim'}$ be an ordered set where $\precsim' \mathop = \subseteq\restriction_{\map {\operatorname{Aux} } R \times \map {\operatorname{Aux} } R}$.

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: \map {\operatorname{Aux} } R \to F$:

$\forall \RR \in \map {\operatorname{Aux} } R: \map G \RR = \paren {S \ni x \mapsto x^\RR}$

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 \RR \in \map {\operatorname{Aux} } R: f = \paren {S \ni x \mapsto x^\RR}$

By definition of image of mapping:

$\forall f \in F: f \in \Img G$

Thus by definition:

$G$ is a surjection.

$\Box$

Order Embedding

Let $\RR, \QQ \in \map {\operatorname{Aux} } R$.

We will prove that:

$\RR \precsim' \QQ \implies \map G \RR \preccurlyeq \map G \QQ$

Let:

$\RR \precsim' \QQ$

By definition of $\precsim'$:

$\RR \subseteq \QQ$

Let $x \in S$.

By Relation Segment is Increasing:

$x^\RR \subseteq x^\QQ$

By Relation Segment of Auxiliary Relation is Ideal:

$x^\RR \in \map {\operatorname{Ids} } R$ and $x^\QQ \in \map {\operatorname{Ids} } R$

By definition of $\precsim$:

$x^\RR \precsim x^\QQ$

By definition of ordering on mappings:

$\paren {S \ni x \mapsto x^\RR} \precsim \paren {S \ni x \mapsto x^\QQ}$

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

$\map G \RR \preccurlyeq \map G \QQ$

$\Box$

We will prove that:

$\map G \RR \preccurlyeq \map G \QQ \implies \RR \precsim' \QQ$

Let:

$\map G \RR \preccurlyeq \map G \QQ$

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

$\paren {S \ni x \mapsto x^\RR} \precsim \paren {S \ni x \mapsto x^\QQ}$

Let $x, y \in S$ such that:

$\tuple {x, y} \in \RR$

By definition of $\RR$-segment:

$x \in y^\RR$

By definition of ordering on mappings:

$y^\RR \precsim y^\QQ$

By definition of $\precsim$:

$y^\RR \subseteq y^\QQ$

By definition of subset:

$x \in y^\QQ$

Thus by definition of $\QQ$-segment:

$\tuple {x, y} \in \QQ$

By definition of subset:

$\RR \subseteq \QQ$

Thus by definition of $\precsim'$:

$\RR \precsim' \QQ$

$\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_4:33