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
- $\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