👋
【領域理論】dcpoの表現【イデアル編】

2025/05/21に公開
 はじめにはじめまして。記事を開いていただきありがとうございます。
本記事では、領域理論におけるdcpoの表現の話の中でも最も重要である抽象基底上のイデアル完備化について解説をします。
表現の話というものは、結局は「あれとこれが対応する」というだけの話に過ぎませんが、ある対象を異なる見方で捉えることがより深い理解につながることは大いによくあることだと思います。（まああまり直接役に立ってる例は私の知識では思いつきませんが）
本記事では、まずは連続dcpoが抽象基底と呼ばれる対象に上手く対応するという事実を理解することを目標に進めていこうと思っております。
抽象基底とイデアル完備化の理論さえ理解できれば、割と他の表現の話も似たようなものなので理解に繋がりやすいんじゃないかなと思っています。
よろしくお願いします。

 ノーテーション有向上限（有向集合のみを定義域に持つ上限）を\sqcupで表す

ゆえに、x=\sqcup Aは「Aは有向集合であり、かつx=\sqcup Aである」という命題と読んでください（x\le\sqcup Aなど他の命題も同様）
この略記法は本記事でも多用しているので十分注意してください

本記事では原則構造付き集合(X, R)とその台集合Xを記法上区別しません
イデアル完備化は本来\mathbf{RI}(B, \prec)のように書くべきですが、本記事では頻繁に\mathbf{RI}(B)と書きます
イデアル完備化\mathbf{RI}(B)自身も(\mathbf{RI}(B), \subseteq)という構造付き集合ですが、勝手に台集合だけ取り出して(\mathbf{RI}(B), \ll)と書くこともあります
同じ台集合上に異なる構造が入る場合には明示することもあります（連続dcpo(D, \le)と基底としての(D, \ll)など）

写像f:X\to Yに対し、A\subseteq Xのfによる像をf[A]と書く

A\subseteq_\mathrm{fin} DはAが有限集合であることを表す

A\subseteq_\mathrm{dir} DはAが有向集合であることを表す
集合A上の二項関係R\subseteq A\times A及びa\in A, X\subseteq Aに対し
XRa\iff\forall x\in X, xRa

aRX\iff\forall x\in X, aRx
特に、posetにおいてはX\le aでaがXの上界であることを表す1



\mathcal K(D)はDのコンパクト元の集合を表す

X\subseteq Dに対し、\mathord\downarrow{X}\coloneqq\{y\in D \mid \exists x\in X, x\le y\}
特に、x\in Dに対し、\mathord\downarrow{x}\coloneqq\mathord\downarrow\{x\}
抽象基底(B, \prec)に対しては、\mathord\Downarrow{A}\coloneqq\{b\in B \mid \exists a\in A, b\prec a\}, \mathord\Downarrow{b}\coloneqq\mathord\Downarrow\{b\}とする

poset P, Qに対し、[P\overset{m}{\to}Q]はposet PからQへの単調写像全体の集合を表す
dcpo D, Eに対し、[D\to E]はdcpo DからEへの連続写像全体の集合を表す

 定義の復習poset Pの部分集合A\subseteq Pが

有向集合：A\not=\emptysetかつ\forall a, b\in A, \exists c\in A, a\le c\land b\le c

下方集合（順序イデアル）：\forall a\in A, \forall b\in P, b\le a\implies b\in A

イデアル：有向下方集合

poset (D, \le)がdcpo：

D上のすべての有向集合は上限をDに持つ

Dは最小元を持つ


x\ll y\iff\forall A\subseteq_\mathrm{dir} D, y\le\sqcup A\implies \exists a\in A, x\le a

x\ll xなる元をDのコンパクト元という

dcpo (D, \le)が連続：
\forall x\in D, x=\sqcup\{y\in D\mid y\ll x\}

dcpo (D, \le)が代数的：
\forall x\in D, x=\sqcup\{c\in\mathcal K(D)\mid c\le x\}

poset間の写像f\colon P\to Qが単調：
\forall a, b\in P, a\le b\implies f(a)\le f(b)

dcpo間の写像f\colon D\to Eが連続：
\forall A\subseteq_\mathrm{dir} D, f(\sqcup A)=\sqcup f[A]


 イデアル完備化連続dcpoと連続写像のなす圏\mathbf{CONT}は抽象基底と近似可能関係[1]のなす圏\mathbf{ABS}と圏同値になります。

 抽象基底とは上限操作で元のdcpo Dの全ての元が復元可能な集合B\subseteq DをDの基底といいます。

 定義1: 基底dcpo Dの部分集合B\subseteq Dは次を満たすときDの基底という。

\forall x\in D, x=\sqcup\{b\in B \mid b\ll x\}
!コンパクト元は常に基底に含まれる、すなわち、\mathcal K(D)\subseteq Bは常に成り立つことに注意してください。特に、最小元は必ずコンパクトなので常に基底に含まれます。

実際、c=\sqcup\{b\in B \mid b\ll c\}ゆえ、コンパクト性の定義より、\exists b\in B, (b\le)c\le bが言えるので、c=b\in Bが言えます。
明らかに、dcpo Dが連続であることと基底を持つことは同値です。

特に、連続dcpo DにおいてはDそのものが基底の一つとなります。
また、dcpo Dが代数的であることとコンパクト元の集合\mathcal K(D)が（最小の）基底をなすことも同値です。
このとき、基底と近似関係の組(B, \ll)が持つ性質を一般化した構造を抽象基底と呼びます。

 定義2: 抽象基底集合B上の二項関係\mathord\prec\subseteq B\times Bが推移的かつ強補間性を満たすとき、(B, \prec)を抽象基底[2] (abstract basis)という。
ただし、集合B上の二項関係\precが強補間性 (strong interpolation property; SIP)を満たすとは、次の条件を満たすことをいう。

\text{(SIP) }\forall b\in B, \forall M\subseteq_\mathrm{fin} B, M\prec b\implies \exists b'\in B, M\prec b'\prec b
また、推移的かつ強補間性を満たす二項関係\precは完全推移的 (fully transitive)と呼ばれる。
抽象基底の定義の補足強補間性について、M=\emptysetとすることにより、任意のb\in Bに対して、b'\prec bなるb'\in Bが存在することが言えます。
ゆえに、\mathord\Downarrow{b}\coloneqq\{b'\in B\mid b'\prec b\}に対して
強補間性：\mathord\Downarrow{b}の非空性と有向性を必要十分に保証
推移性：　\mathord\Downarrow{b}の下方性を必要十分に保証
言い換えれば、単項イデアルが確かにイデアルとなっていることを保証する必要十分な構造が抽象基底となっているわけになります。
また後に説明しますが、抽象基底のイデアル完備化においては\{\mathord\Downarrow{b}\mid b\in B\}が基底をなすという事実が非常に重要であり、また別の言い方をすれば抽象基底とはイデアル完備化によりdcpoを得るための最小限の構造であるとも言えます。
基底と近似関係の組(B, \ll)は抽象基底をなすことが補題3より直ちに従います。

 補題3: 近似関係の性質dcpo (D, \le)に対し、近似関係\mathord{\ll}\subseteq D\times Dは次の性質を満たす。
x\ll y\implies x\le y
x\le y\ll u\le v\implies x\ll v
(推移性)

x\ll y\text{ and }y\ll z\implies x\ll z
さらに、(D, \le)が連続ならば次も満たす。基底B_D\subseteq Dを取る。
(強補間性)

M\ll z\implies \exists v\in B_D, M\ll v\ll z\text{ for } M\subseteq_\mathrm{fin} D
(連続性)

連続dcpoD, Eに対し、基底B_D, B_Eを取る。D, E間の単調関数f\colon D\to Eに対し、fが連続であることと、任意のx\in D, c\in B_Eに対し次が成り立つことは同値である。

c\ll_E f(x)\implies\exists b\in B_D, c\ll_E f(b)\land b\ll_D x
証明1の証明今、y\le\sqcup\{y\}(=y)なので、\exists z\in\{y\}, x\le z、すなわち、x\le y
2の証明有向集合A\subseteq_\mathrm{dir} Dに対し、v\le\sqcup Aと仮定すると、u\le vより、u\le\sqcup Aとなる。

y\ll uより、\exists a\in A, y\le aだが、x\le yより\exists a\in A, x\le aとなる。

したがって、x\ll vが言えた。
3（推移性）の証明有向集合A\subseteq_\mathrm{dir} Dに対し、z\le\sqcup{A}と仮定すると、y\ll zより、\exists a\in A, y\le aとなる。

性質1より、x\ll yからx\le yが言えるので、\exists a\in A, x\le aとなる。
4（強補間性）の証明A=\{u\in D\mid\exists v\in B_D, u\ll v\ll z\}とする。

このとき、Aは有向集合であり（※1）、z=\sqcup Aが言える（※2）。

ゆえに、M\ll zより、各x\in Mに対して\exists u_x\in A, x\le u_xなためu_xの上界u\in Aに対してAの定義より\exists v\in B_D, u\ll v\ll zゆえ、M\le u\ll v\ll zとなる。（M=\emptysetならu=\bot\in Aを取れば良い。）

つまり、性質2より、M\ll v\ll zが言えた。
（※1）Aの有向性について\bot\in AよりA\not=\emptysetである。u_1, u_2\in Aに対し、u_1, u_2\le v\in Aなるvの存在を示す。

まずAの定義より\exists v_1, v_2\in B_D, u_1\ll v_1\ll zかつu_2\ll v_2\ll z

Dは連続より、\{y\in B_D\mid y\ll z\}は有向集合であるため、\exists v\in D, v_1, v_2\le v\ll z

性質2よりu_1, u_2\ll vであり、再び\{y\in B_D\mid y\ll v\}の有向性より、\exists u\in B_D, u_1, u_2\le u\ll v(\ll z)が言え、u_1, u_2\le u\in A
（※2）z=\sqcup AについてA\le zは明らかより、他の上界wに対しz\le wを示す。

これは、「\forall v\in D, v\ll z\implies v\le w」（\because v=^{\text{※3}}\sqcup\{u\in D\mid u\ll v(\ll z)\}\le\sqcup A\le w）からz=^{\text{※3}}\sqcup\{v\in D\mid v\ll z\}\le wとなり証明完了。（※3 by continuity of D）
5（連続性）の証明
\impliesについてc\ll_E f(x)とする。強補間性より、c\ll_E c'\ll_E f(x)なるc'\in B_Eが存在する。

今、基底の定義より、x=\sqcup\{b\in B_D \mid b\ll_D x\}なので、fの連続性を用いてf(x)=\sqcup\{f(b)\mid b\ll_D x, b\in B_D\}が言える。
よって、c'\ll_E f(x)だったので、近似関係の定義からあるb\ll_D xなるb\in Bで、(c\ll_E)c'\le_E f(b)となる。
ゆえに、補題3-2より、c\ll_E f(b)が言える。

\impliedbyについて任意のA\subseteq_\mathrm{dir} Dに対し、f(\sqcup A)=\sqcup f[A]を示す。

まず、fの単調性より、任意のa\in Aに対しf(a)\le_E f(\sqcup A)が言えるため、\sqcup f[A]\le_E f(\sqcup A)が言える。
逆に、f(\sqcup A)\le_E\sqcup f[A]を示す。

今、任意のx, y\in Eに対し、B_E\cap\mathord\Downarrow{x}\subseteq B_E\cap\mathord\Downarrow{y}を示せば、x=\sqcup(B_E\cap\mathord\Downarrow{x})\le_E\sqcup(B_E\cap\mathord\Downarrow{y})=yが言える。

（ただし、\mathord\Downarrow{x}\coloneqq\{y\in E\mid y\ll_E x\}で定義する）
したがって、\forall c\in B_E, c\ll_E f(\sqcup A)\implies c\ll_E\sqcup f[A]を示せばよい。
c\in B_Eに対し、c\ll_E f(\sqcup A)と仮定する。

命題の仮定より、\exists b\in B_D, c\ll_E f(b)\land b\ll_D\sqcup Aが言える。

近似関係の定義より、あるa\in Aでb\le_D aゆえ、fの単調性より(c\ll_E)f(b)\le_E f(a)(\le_E\sqcup f[A])が言える。

よって、補題3-2より、c\ll_E\sqcup f[A]となるため、f(\sqcup A)\le_E\sqcup f[A]が証明できた。

\square

 定理4: 基底は抽象基底をなす基底B\subseteq Dを持つdcpo (D, \le)に対し、(B, \ll)は抽象基底をなす。
反射性は強補間性を明らかに含意するので、完全推移的関係は前順序の一般化と捉えられます。

すなわち、前順序集合及び半順序集合はともに抽象基底をなすことがわかります。
特に、代数的dcpoのコンパクト基底(\mathcal K(D), \ll)は半順序としての抽象基底をなします。

 命題5: コンパクト元による近似関係dcpo (D, \le)に対し、次が成り立つ。

\forall x\in D, \forall c\in\mathcal K(D), c\ll x\iff c\le x
特に、(\mathcal K(D), \ll)は(\mathcal K(D), \le)と一致する。
証明\impliesは補題3-1。\impliedbyはc\ll c\le xゆえc\ll x (\because 補題3-2)

 イデアル完備化とは基底B\subseteq Dからx\in Dを復元するには\{b\in B \mid b\ll x\}の上限を取ればよいのでした。
では、Dが与えられずに抽象基底(B, \prec)のみが与えられたときは、どのように元x\in Dを復元すればよいのでしょうか。

xに収束する集合\{b\in B \mid b\prec x\}の上限を取りたいのですが、そもそも我々はxを知りませんし、Bはdcpoではないので上限操作は定義されていません。
後者の問題は、上限を取らなくても\{b\in B \mid b\prec x\}という集合そのものをxとみなすことで解決できます。

前者の問題は、xを明示せずとも我々の知らない「何か」に収束しそうな集合を考えることで解決できます。
領域理論では、有向集合をもって「何か」に収束しそうな集合と捉えます。

さらに、同じ収束先を持つ集合をまとめるために（「収束先が同じ」という同値関係で割ってもよいのですが、簡単のために）下方集合のみを考えることにします。[3]
このとき、有向下方集合をイデアルと呼び、基底上のイデアル全体を考えることで抽象基底のみが与えられたとしても想定されていたdcpo Dを復元することができます。
ただし、イデアルとは通常は半順序上（せめて前順序上）でのみ定義される概念であり、抽象基底上で有向性と下方性を同様に定義して得られるイデアルはしばしばround idealと呼ばれます。

 定義6: イデアル(B, \prec)を抽象基底とする。A\subseteq Bの有向性・下方性を次のように定義する。

Aが有向集合：A\not=\emptysetかつ\forall a, b\in A, \exists c\in A, a\prec c\land b\prec c

Aが下方集合：A=\mathord\Downarrow{A}\text{ i. e. }\forall a\in A, \forall b\in B, b\prec a\implies b\in A
Bの有向下方集合I\subseteq Bをround idealと呼ぶ。
特に、\precが反射的、すなわち、(B, \prec)が前順序をなすときIは単にイデアルと呼ばれる。
一般に、抽象基底Bの部分集合A\subseteq Bが極大元を持たないとき、Aはroundedと呼ばれます。おそらく尖ってないみたいなイメージかなと思っています。

round idealは有向性により常にroundedとなり、特に前順序集合上のイデアルは常に自分自身によりtrivialにroundedです。
!通常は前順序集合(P, \le)上の極大元といったら、狭義順序<に関する極大元を指すことが暗黙の了解ですが、ここでは言葉通り\leに関する極大元を指していることに注意してください。
roundnessの補足抽象基底(B, \prec)の反射閉包、すなわち、前順序集合(B, \preceq)上のイデアルI\subseteq Bについて、次のような特徴付けが可能です。

I\text{ is rounded w.r.t. }\mathord\prec\iff I \text{ is a round ideal of } (B, \prec)
つまり、round idealはまさにroundedなイデアルと考えられます。

逆に（通常の）イデアルとは反射性によりある種のroundnessが潰れてしまったround idealとも考えられます。（trivialにはroundedです）
以降では簡単のためにround idealも単にイデアルと呼ぶことにします。

 定義7: イデアル完備化抽象基底(B, \prec)上のイデアルすべての集合を\mathbf{RI}(B)とする。

このとき、poset (\mathbf{RI}(B), \subseteq)をBのイデアル完備化と呼ぶ。
抽象基底のイデアル完備化により連続dcpoが得られます。[4]

 補題8: イデアル完備化の性質(B, \prec)を抽象基底とする。

(\mathbf{RI}(B), \subseteq)はdcpoをなす。

x\in Bに対し、\mathord\Downarrow{x}\in\mathbf{RI}(B)である。

I\in\mathbf{RI}(B)に対し、I=\bigcup\{\mathord\Downarrow{x}\mid x\in I\}

I\in\mathbf{RI}(B)に対し、I=\bigcup\{\mathord\Downarrow{x}\mid\mathord\Downarrow{x}\ll I\}
I_1\ll I_2\iff\exists x\in I_2, I_1\subseteq\mathord\Downarrow{x}
I_1\ll I_2\iff\exists x\in I_2, I_1\ll\mathord\Downarrow{x}

b_1, b_2\in Bに対し、\mathord\Downarrow{b_1}\ll\mathord\Downarrow{b_2}\iff b_1\prec b_2

\{\mathord\Downarrow{x}\mid\mathord\Downarrow{x}\ll I\}は有向集合。
証明補題8-1の証明有向完備性について有向集合\mathcal A\subseteq_\mathrm{dir} \mathbf{RI}(B)に対し、\bigcup\mathcal Aが\mathcal Aの上限であること、すなわち、B上のイデアルであることを示す。
有向性について

x, y\in\bigcup\mathcal Aとすれば、あるイデアル I_1, I_2\in\mathcal Aが存在してx\in I_1, y\in I_2である。

\mathcal Aの有向性より、\exists I\in\mathcal A, I_1, I_2\subseteq Iが言える。

つまり、x, y\in IからI自体の有向性より、\exists z\in I\subseteq\bigcup\mathcal A, x, y\prec z
下方性について

z\in\bigcup\mathcal Aとすれば、あるイデアル I\in\mathcal Aが存在してz\in Iである。

z\in Iより、Iの下方性より、\forall x\in B\text{ s.t. }x\prec z, x\in I\subseteq\bigcup\mathcal Aが言える。
したがって、\bigcup\mathcal AはB上のイデアルである。
最小元についてBが最小元\botを持つならば、\mathbf{RI}(B)の最小元は\mathord\Downarrow{\bot}=\{\bot\}である。

（Bに最小元がなければ\mathbf{RI}(B)も最小元を持たない）
補題8-2の証明下方性は推移性より明らか。強補間性にてM=\emptysetとすることで\mathord\Downarrow{x}\not=\emptysetもわかる。最後に、y, z\in\mathord\Downarrow{x}ならy, z\prec xゆえ強補間性より\exists w\in B, y, z\prec w\prec x
補題8-3の証明
\bigcup\{\mathord\Downarrow{x}\mid  x\in I\}\subseteq Iについてx\in Iに対し、i(x)=\mathord\Downarrow{x}\subseteq Iより、\bigcup\{\mathord\Downarrow{x}\mid  x\in I\}\subseteq I

I\subseteq\bigcup\{\mathord\Downarrow{x}\mid  x\in I\}についてx\in Iとすると、Iのroundness（有向性）より\exists y\in I, x\prec y(\iff x\in\mathord\Downarrow{y})ゆえに、x\in\bigcup\{\mathord\Downarrow{x}\mid  x\in I\}となる。
補題8-4の証明まず、x\in I\implies\mathord\Downarrow{x}\ll Iを示す。

有向集合\mathcal A\subseteq_\mathrm{dir}\mathbf{RI}(B)に対し、(x\in)I\subseteq\bigcup\mathcal Aとする。

よって、あるI'\in\mathcal Aでx\in I'、ゆえに、\mathord\Downarrow{x}\subseteq I'となる。

したがって、\mathord\Downarrow{x}\ll I
以上より、\{\mathord\Downarrow{x}\mid x\in I\}\subseteq\{\mathord\Downarrow{x}\mid \mathord\Downarrow{x}\ll I\}が成り立つ。

よって、補題8-3よりI=\bigcup\{\mathord\Downarrow{x}\mid x\in I\}\subseteq\bigcup\{\mathord\Downarrow{x}\mid\mathord\Downarrow{x}\ll I\}\subseteq Iである。

（最後の包含：\mathord\Downarrow{x}\ll I\implies\mathord\Downarrow{x}\subseteq I　\because 補題3-1 ）
すなわち、I=\bigcup\{\mathord\Downarrow{x}\mid\mathord\Downarrow{x}\ll I\}
補題8-5の証明
\impliesについて補題8-3よりI_2=\bigcup\{\mathord\Downarrow{x}\mid x\in I_2\}ゆえ、I_1\ll I_2より\exists x\in I_2, I_1\subseteq\mathord\Downarrow{x}

\impliedbyについて今、あるx\in I_2に対し、I_1\subseteq\mathord\Downarrow{x}とする。

有向集合\mathcal A\subseteq_\mathrm{dir}\mathbf{RI}(B)に対し、I_2\subseteq\bigcup\mathcal Aとすると、あるI\in\mathcal Aでx\in I、ゆえに、I_1\subseteq\mathord\Downarrow{x}\subseteq Iとなる。

したがって、I_1\ll I_2が成り立つ。
補題8-6の証明
\impliesについて強補間性より、あるI\in\mathbf{RI}(B)でI_1\ll I\ll I_2となる。

補題8-5より、\exists x\in I_2, (I_1\ll)I\subseteq\mathord\Downarrow{x}が成り立つ。

よって、補題3-2より、I_1\ll\mathord\Downarrow{x}が成り立つ。

\impliedbyについてI_1\ll\mathord\Downarrow{x}より、\mathord\Downarrow{x}\subseteq I_2が成り立ち、補題8-5より、I_1\ll I_2となる。
補題8-7の証明
\impliedbyについて強補間性より、あるb\in Bでb_1\prec b\prec b_2であり、\mathord\Downarrow{b_1}\subseteq\mathord\Downarrow{b}が成り立つ。ゆえに、補題8-5より\mathord\Downarrow{b_1}\ll\mathord\Downarrow{b_2}となる。

\impliesについてこれホンマに成り立つんか？？？ n時間考えてたけどわからない。

Scottらの"Continuous Lattices and Domains"の250ページのExercise III-4.17 (iii)の"In particular..."の部分を参照してください。
補題8-8の証明\mathord\Downarrow{x}, \mathord\Downarrow{y}\ll Iとすれば、補題8-5よりあるz_1, z_2\in Iに対し、\mathord\Downarrow{x}\subseteq\mathord\Downarrow{z_1}, \mathord\Downarrow{y}\subseteq\mathord\Downarrow{z_2}が成り立つ。

Iの有向性より、\exists z\in I, z_1, z_2\prec zが成り立ち、\mathord\Downarrow{x}, \mathord\Downarrow{y}\subseteq\mathord\Downarrow{z}が成り立つ。

さらに、roundnessから、z\prec z'\in Iなるz'が存在し、\mathord\Downarrow{z}\subseteq\mathord\Downarrow{z'}が成り立つ。

したがって、補題8-5より\mathord\Downarrow{z}\ll Iが成り立つ。

\square

 定理9: 抽象基底のイデアル完備化は連続抽象基底(B, \prec)のイデアル完備化(\mathbf{RI}(B), \subseteq)は連続dcpoをなす。[5]
証明補題8-1よりdcpoとなる。連続性について。

i\colon B\to\mathbf{RI}(B); x\mapsto\mathord\Downarrow{x}に対して、i[B]=\{\mathord\Downarrow{x}\mid x\in B\}は\mathbf{RI}(B)の基底をなすことを示せばよい。
補題8-8より\{i(x)\mid i(x)\ll I\}は有向集合であり、補題8-4より、I=\bigcup\{i(x)\mid i(x)\ll I\}が成り立つ。
したがって、(\mathbf{RI}(B), \subseteq)は連続dcpoをなす。

\square
!i\colon B\to\mathbf{RI}(B); x\mapsto\mathord\Downarrow{x}は単射とは限らないことに注意してください。
例：iが単射とならないケース

B=\{a, b\}, a\preceq b\preceq aなる（抽象基底としての）前順序集合を考えれば、a\not=bだがi(a)=i(b)=\{a, b\}となる。
例：有理数の完備化

round ideal完備化の代表例は有理数の完備化です。\R_\infty\coloneqq\R\cup\{\infty\}とします。

(\mathbb{Q}, <)は確かに抽象基底をなし、そのイデアル完備化は(\R_\infty, \le)と同型になります。

これはデデキントカットそのものであり、つまりデデキントカットはround ideal完備化の代表例になっています。

ちなみに、\R_\inftyは連続だが代数的でないdcpoの代表例です。（最小元が気になる人は0以上とかで考えてください）

\square
このとき、イデアル完備化は弱い普遍性を満たします。

 定理10: イデアル完備化の普遍性抽象基底(B, \prec), dcpo (D, \le)に対し、イデアル完備化は次の弱い普遍性を満たす。
\begin{array}{ccc}
B & &\\
\mathord\downarrow i & \overset{f}{\searrow} & \\
\mathbf{RI}(B) & \overset{\hat{f}}{\dashrightarrow} & D
\end{array}すなわち、任意の単調写像f\colon B\to Dに対し、\hat{f}\circ i\le fを満たす最大の連続写像\hat{f}\colon \mathbf{RI}(B)\to Dが（最大性より一意に）存在し、\hat{f}(I)=\sqcup f[I]で与えられる
このとき、さらに次も成り立つ。

h(f)=\hat{f}: [B\overset{m}{\to} D]\to[\mathbf{RI}(B)\to D]は連続写像

\precが反射的（すなわち、前順序集合のイデアル完備化の場合）ならば\hat{f}\circ i=f
証明\hat{f}(I)\coloneqq\sqcup f[I]が定理の条件を満たすことを言えば良い。

証明にはposetにおける常套手法である次の有名定理を用いる。

(\forall c\in P, b\le c\implies a\le c)\iff a\le b

\hat{f}の連続性有向集合\mathcal A\subseteq_\mathrm{dir}\mathbf{RI}(B)を固定する。

\hat{f}の単調性をまず示す。I_1\subseteq I_2とすれば、fの単調性よりf[I_1]\subseteq f[I_2]ゆえ、 \hat{f}(I_1)=\sqcup f[I_1]\le\sqcup f[I_2]=\hat{f}(I_2)が言え、\hat{f}は単調。
次に、有向集合\mathcal Aに対し、\hat{f}(\bigcup\mathcal A)=\sqcup \hat f[\mathcal A]を示す。（\hat{f}の単調性よりf[\mathcal A]は有向）

\begin{array}{cll}
&& \sqcup \hat f[\mathcal A]\le d_0 \\
\iff & \forall I\in\mathcal A, & \hat f(I)\le d_0 \\
\iff & \forall I\in\mathcal A, & \sqcup f[I]\le d_0 \\
\iff & \forall I\in\mathcal A, \forall x\in I, & f(x)\le d_0 \\ 
\iff & \forall x\in\bigcup\mathcal A, & f(x)\le d_0 \\
\iff && \sqcup f[\bigcup\mathcal A]\le d_0 \\
\iff && \hat f(\bigcup\mathcal A)\le d_0 \\
\end{array}
したがって、\hat{f}(\bigcup\mathcal A)=\sqcup \hat f[\mathcal A]

\hat{f}\circ i\le fについて任意のx\in Bに対し、\hat{f}\circ i(x)\le f(x)を示す。

\begin{array}{cll}
&& f(x)\le d_0 \\
\implies & \forall y\prec x, & f(y)\le d_0 \\
\iff & \forall y\in\mathord\Downarrow{x}, & f(y)\le d_0 \\
\iff && \sqcup f[\mathord\Downarrow{x}]\le d_0 \\
\iff && \hat f(\mathord\Downarrow{x})\le d_0 \\
\iff && \hat f\circ i(x)\le d_0 \\
\end{array}
したがって、\hat{f}\circ i\le f

\hat{f}の最大性について他にg\circ i\le fを満たす連続写像g\colon \mathbf{RI}(B)\to Dがあったとき、g\le \hat{f}を示す。すなわち、任意のI\in\mathbf{RI}(B)に対し、g(I)\le \hat{f}(I)を示せばよい。

\begin{array}{cll}
&& \hat f(I)\le d_0 \\
&& \sqcup f[I]\le d_0 \\
\iff & \forall x\in I, & f(x)\le d_0 \\
\implies & \forall x\in I, & g\circ i(x)\le d_0 \\
\iff & \forall x\in I, & g(\mathord\Downarrow{x})\le d_0 \\
\iff && \sqcup_{x\in I}g(\mathord\Downarrow{x})\le d_0 \\
\iff && g(\sqcup_{x\in I}\mathord\Downarrow{x})\le d_0 \\
\iff && g(I)\le d_0 \\
\end{array}
したがって、g\le \hat{f}
性質1についてh=f\mapsto\hat{f}\colon[B\overset{m}{\to} D]\to[\mathbf{RI}(B)\to D]とする。

hの単調性f_1\le f_2のとき、\sqcup f_1[I]\le\sqcup f_2[I]が成り立つため、h(f_1)=\hat{f}_1(I)\le\hat{f}_2(I)=h(f_2)となり、hは単調。

hの連続性有向集合F\subseteq_\mathrm{dir}[B\overset{m}{\to} D]に対し、h(\sqcup F)=\sqcup h[F]を示す。

\begin{array}{cll}
&& \sqcup h[F]\le f_0 \\
\iff & \forall f\in F, & \hat f\le f_0 \\
\iff & \forall f\in F, \forall I\in\mathbf{RI}(B), & \hat{f}(I)\le f_0(I) \\
\iff & \forall f\in F, \forall I\in\mathbf{RI}(B), & \sqcup f[I]\le f_0(I) \\
\iff & \forall f\in F, \forall I\in\mathbf{RI}(B), \forall x\in I, & f(x)\le f_0(I) \\
\iff & \forall I\in\mathbf{RI}(B), \forall x\in I, & \sqcup_{f\in F} f(x)\le f_0(I) \\
\iff & \forall I\in\mathbf{RI}(B), \forall x\in I, & (\sqcup F)(x)\le f_0(I) \\
\iff & \forall I\in\mathbf{RI}(B), & \sqcup(\sqcup F)[I]\le f_0(I) \\
\iff & \forall I\in\mathbf{RI}(B), & h(\sqcup F)(I)\le f_0(I) \\
\iff && h(\sqcup F)\le f_0 \\
\end{array}
したがって、h(\sqcup F)=\sqcup h[F]が成り立つ。
性質2について\hat{f}\circ i\le fの証明で\impliesとなっている行の逆を示せばよい。

すなわち、\forall y\prec x, f(y)\le d_0\implies f(x)\le d_0を示せばよいが、\precが反射的ゆえ仮定ににおいてyとしてxを取ればよい。

\square
B_Dがdcpo Dの基底だった際に、単調写像f\colon B_D\to Dとして自然と包含写像を考えることができます。（x\ll y\implies x\le yに注意）

その際、イデアル完備化の（弱い）普遍性から得られる写像は有向上限\sqcup\colon\mathbf{RI}(B_D)\to Dとなり、これは\mathbf{RI}(B_D)\cong Dの同型を与えます。
すなわち、連続dcpoは基底からイデアル完備化を取ることで復元可能となります。

 定理11: 連続dcpoは基底から復元可能 (D\cong\mathbf{RI}(B_D))
連続dcpo (D, \le)及びその基底(B_D, \ll)に対し、包含写像をe(x)\coloneqq x\colon B_D\to Dとする。

このとき、\hat e\colon \mathbf{RI}(B_D)\to Dは同型写像であり、逆写像は\beta(x)\coloneqq\{b\in B_D\mid b\ll x\}:D\to\mathbf{RI}(B_D)で与えられる。
証明連続性は定理9で言えているため、全単射であることを示せば良い。
1. \hat e\circ\beta =\mathrm{id}_Dについて\hat e\circ\beta(x)=\hat e(\{b\in B_D\mid b\ll x\})=\sqcup \{b\in B_D\mid b\ll x\}=x
2. \beta\circ\hat e =\mathrm{id}_{\mathbf{RI}(B_D)}について\beta\circ\hat e(I)=\beta(\sqcup I)=\{b\in B_D\mid b\ll \sqcup I\}だが、次を示せば\beta\circ\hat e(I)が言える。

\forall b\in B_D, b\ll\sqcup I\iff b\in I

\impliesについて近似関係の強補間性より、あるx\in Dが存在しb\ll x\ll\sqcup Iとなる。

よって近似関係の定義より、\exists b'\in I, (b\ll)x\le b'ゆえ、補題3-2よりb\ll b'(\in I)となる。

(B_D, \ll)上のイデアルIの下方性より、b\in I

\impliedbyについて(B_D, \ll)上のイデアルIのroundnessより、\exists b'\in I, b\ll b'(\le\sqcup I)ゆえ、b\ll\sqcup Iとなる。

\square
つまり、基底上のイデアルは元のdcpoの元を上限操作により必要十分に表せていたということになり、我々は勝手に「何かに収束しそうな集合 = （下方な）有向集合」としましたが数学的に妥当な捉え方だった事がわかりました。

 イデアル完備化と代数性イデアル完備化は連続ですが、一般には代数的とは限りません。

式I=\bigcup\{\mathord\Downarrow{x}\mid  x\in I\}において\mathord\Downarrow{x}らがコンパクト元をなすと限らず、コンパクト元のみでIを復元できるとは限らないためです。
抽象基底上のイデアルIが一元生成、すなわち、\mathord\Downarrow{x}の形であるときIを単項イデアルと呼びます。

しかし、抽象基底においては単項イデアル\mathord\Downarrow{x}は必ずしもxを含むとは限らず、ゆえにコンパクト性が失われています。
そこで、x\in\mathord\Downarrow{x}となる単項イデアルを主イデアルと呼びます。

 補題12: 主イデアルの性質抽象基底(B, \prec)上のb\in B, I\in\mathbf{RI}(B)に対し、次が成り立つ。（証明は容易）

\mathord\Downarrow{b}は主イデアル\iff b\prec b

Iはコンパクト\iff Iは主イデアル

\mathord\Downarrow{b}が主イデアルのとき、\mathord\Downarrow{b}\ll I\iff\mathord\Downarrow{b}\subseteq I\iff b\in I
このとき、イデアル完備化が代数的となる境界条件は次で与えられます。

 定理13: イデアル完備化が代数的となる条件抽象基底(B, \prec)に対し、次が成り立つ。

\mathbf{RI}(B) \text{ is algebraic }\iff C=\{c\in B\mid c\prec c\} \text{ is dense in } B
ただし、抽象基底Bの部分集合C\subseteq BがBにおいて稠密 (dense)であるとは、次を満たすことをいう。

\forall x\prec y\in B, \exists c\in C, x\prec c\prec y
証明
\impliesについて\mathbf{RI}(B)の代数性より、各y\in Bに対し\mathord\Downarrow{y}=\bigcup_{\mathord\Downarrow{y}\supseteq I\text{: cpt}}I=\bigcup_{c\prec c\prec y}\mathord\Downarrow{c}となる。（\because 補題12）

したがって、x\prec yに対し、\exists c\in C, x\in\mathord\Downarrow{c}となるため、\exists c\in C, x\prec c\prec yが言えた。

\impliedbyについて補題12を用いることで、任意のI\in\mathbf{RI}(B)に対しI=\bigcup_{c\prec c\in I}\mathord\Downarrow{c}を示せばよい。（※1）
\supseteqについて

\bigcup_{c\prec c\in I}\mathord\Downarrow{c}\subseteq\bigcup_{x\in I}\mathord\Downarrow{x}=I（最後の等号は補題8-3より）
\subseteqについて

x\in Iとすると、Iのroundnessより、あるy\in Iでx\prec yとなる。

Cの稠密性より、\exists c\in C, x\prec c\prec yゆえに、\exists c\in C, x\in\mathord\Downarrow{c}、すなわち、x\in\bigcup_{c\prec c\in I}\mathord\Downarrow{c}が言えた。
※1. A=\{\mathord\Downarrow{c}\mid c\prec c\in I\}の有向性について任意に\mathord\Downarrow{c_1}, \mathord\Downarrow{c_1}\in Aを取る。c_1, c_2\in I\cap Cに対し、Iの有向性よりc_1, c_2\prec xなるx\in Iが存在。

さらに、Iのroundnessより、x\prec yなるy\in Iが存在する。

Cの稠密性よりx\prec c\prec yなるc\in Cが存在し、Iの下方性よりc\in Iとなる。

ゆえに、c_1, c_2\prec c\in I\cap Cなるcが存在し、\mathord\Downarrow{c_1}, \mathord\Downarrow{c_2}\subseteq\mathord\Downarrow{c}\in Aが言える。

\square
抽象基底が反射的、すなわち、前順序集合なら明らかにC=\{c\in B\mid c\prec c\}=Bとなるため、Cは確実にBにおいて稠密となります。

特に、代数的dcpoのコンパクト基底(\mathcal K(D), \ll)はposetをなすため、確かにコンパクト基底のイデアル完備化からは代数的dcpoが得られます。（定理11より元の代数的dcpoに一致する）

 近似可能関係抽象基底は連続dcpoにある程度対応する構造であることがわかりました。

続いて、連続写像に対応する抽象基底間の関係を考えてみましょう。
まず、ぱっと思いつくのは単に連続写像f\colon D\to Eの定義域をDの基底B_Dに制限した単調写像f'\colon B_D\to Eを得ることです。

確かに、このf'から定義域のイデアル完備化により元のfを復元することができます。
しかし、今考えたいのは抽象基底間の関係であり、b\in B_Dに対してf(b)がEの基底の元であるとは限りません。

そこで、次の試みとしてf'をEの基底B_Eのイデアル完備化への写像f''\colon B_D\to\mathbf{RI}(B_E); b\mapsto\mathord\Downarrow{f(b)}とします。
確かに、定義には基底の元しか登場していないため、十分上手くいっていると思います。

しかし、やはり我々は純粋に抽象基底間の関係を考えたいため少し不満が残ります。
そこで、思い切って写像であることを諦めることにしましょう。

bを\mathord\Downarrow{f(b)}に写すのではなく、\mathord\Downarrow{f(b)}内の全ての元に写す多価関数のような関係を考えます。

すなわち、b\mathrel{R}c\iff c\in\mathord\Downarrow{f(b)}(\iff c\ll_E f(b))というような関係R\subseteq B_D\times B_Eを考えます。
このとき、Rは次を満たしているはずです。
任意のb\in B_Dに対し、\{c\in B_E\mid b\mathrel{R}c\}はイデアルをなす（つまり、\mathord\Downarrow{f(b)}がイデアルをなす）

b_1\ll_D b_2\in B_Dに対し、\{c\in B_E\mid b_1\mathrel{R}c\}\subseteq\{c\in B_E\mid b_2\mathrel{R}c\}となる（つまり、f''の単調性）
また、さらにRが連続dcpo間の連続写像に対応することも忘れてはいけません。

連続dcpo間の連続写像は、補題3-5による基底と近似関係のみを用いた特徴付けが可能でした。こちらも定義に加えましょう。
このような、抽象基底間における連続写像の対応物を近似可能関係 (approximable relation) と呼びます。

 定義14: 近似可能関係抽象基底(B, \prec_B), (C, \prec_C)に対し、関係R\subseteq B\times Cが次を満たすときRを近似可能関係といい、R\colon B\to Cと書く。

（ごちゃごちゃするので\forallは省きました。ただし、MはCの任意の有限部分集合です）
（単調性）：b_2\succ b_1\mathrel{R}c\implies b_2\mathrel{R}c

（下方性）：b\mathrel{R}c_2\succ c_1\implies b\mathrel{R}c_1

（有向性）：b\mathrel{R}M\implies\exists c\in C, b\mathrel{R}c\succ M

（連続性[6]）：b_2\mathrel{R}c\implies\exists b_1\in B, b_1\succ b_2\mathrel{R}c
!ストリクトな連続関数に対応する近似関係を定義する場合は\bot_B\mathrel{R}c\iff c=\bot_Cの条件も加える必要があります。
今、R(b)\coloneqq\{c\in C\mid b\mathrel{R}c\}と定義すれば（下方性）及び（有向性）よりR(b)\in\mathbf{RI}(C)がわかります。

さらに、（単調性）よりR\colon B\to\mathbf{RI}(C)は単調写像となります。
ところで、向きを反転させた\succ_B\colon B\to Bは明らかに近似可能関係であり、さらに他の任意のR\colon B\to C, S\colon C\to Bに対し、R\circ\mathord\succ_B=R, \mathord\succ_B\circ S=Sが成り立ちます。[7]

また、近似可能関係の合成も常に近似可能関係です。
!\mathrm{id}\coloneqq\{(b, b)\mid b\in B\}は近似可能関係ではないことに注意してください。

連続写像f\colon D\to Eに対応する近似可能関係がb\mathrel{R_f}c\iff c\ll f(b)だったことを思い返せば、むしろ連続写像としての\mathrm{id}\colon D\to Eに対応する近似関係がb\mathrel{R_\mathrm{id}}c\iff b\gg cであることがわかります。
そこで、近似可能関係のもと抽象基底間の同型性を定義します。

 定義15: 抽象基底間の同型性抽象基底(B, \prec_B), (C, \prec_C)に対し、近似可能関係R\colon B\to Cが次を満たすとき、Rを同型（射）という。
\exists S\colon C\to B, R\circ S=\mathord\succ_C\text{ and }S\circ R=\mathord\succ_B今、抽象基底B, Cに対し、同型R\colon B\to Cが存在するとき、BとCは同型であるといい、B\cong Cと書く。
!抽象基底は同型でもサイズが等しいとは限りません。
例：サイズの異なる同型な抽象基底

（抽象基底としての）前順序集合(B, \preceq_B), (C, \preceq_C)を次で定義する。

すなわち、前者はB=\{a, b, c\}で巡回前順序a\preceq_Bb\preceq_Bc\preceq_Baを持つとし、後者はC=\{*\}で*\preceq_C*なる順序を持つとする。
そのとき、R=\{(a, *), (b, *), (c, *)\}\colon B\to Cとすれば、Rは同型となる。
実際、S=\{(*, a), (*, b), (*, c)\}\colon C\to Bとすれば、R\circ S=\mathord\succeq_C及びS\circ R=\mathord\succeq_Bが成り立つ。
このとき、定理11の逆の関係が言えます。すなわち、任意の抽象基底はそのイデアル完備化から復元可能となります。

 定理16: 抽象基底はイデアル完備化から復元可能 (B\cong B_{\mathbf{RI}(B)})
抽象基底(B, \prec)及びイデアル完備化\mathbf{RI}(B)の基底B_{\mathbf{RI}(B)}\coloneqq i[B]\coloneqq\{\mathord\Downarrow{b}\mid b\in B\}に対し、
\theta\coloneqq\{(b_2, \mathord\Downarrow{b_1})\mid b_2\succ b_1\in B\}\colon B\to B_{\mathbf{RI}(B)}
\phi\coloneqq\{(\mathord\Downarrow{b_2}, b_1)\mid b_2\succ b_1\in B\}\colon B_{\mathbf{RI}(B)}\to B
と定めると、\phi\circ\theta=\mathord\succ及び\theta\circ\phi=\mathord\ggが成り立つ。

すなわち、\thetaは同型であり、B\cong B_{\mathbf{RI}(B)}が成り立つ。
証明補題8-6により、b_1\prec b_2\iff\mathord\Downarrow{b_1}\ll\mathord\Downarrow{b_2}に注意する。
また、i(b)\coloneqq\mathord\Downarrow{b}は単射じゃないが、\thetaの元(b_2, I)を適当に取ったとき定義よりb_2\succ b_1かつI=\mathord\Downarrow{b_1}なるb_1\in Bが存在するため、以降では最初からそのようなb_1の一つを取っているとして、\thetaの元を(b_2, \mathord\Downarrow{b_1})のように書くとする。

\theta, \phiは近似可能関係\thetaが近似可能関係であることを示す。（\phiについても全く同様に示せる）
単調性

b_2\succ b_1\mathrel{\theta}\mathord\Downarrow{b_0}とすれば、定義よりb_0\prec b_1なので推移性からb_0\prec b_2となる。
下方性

b_2\mathrel{\theta}\mathord\Downarrow{b_1}\gg\mathord\Downarrow{b_0}とすれば、b_1\succ b_0より推移性からb_2\succ b_0となる。
有向性

b_2\mathrel{\theta}Mとすれば、各\mathord\Downarrow{b}\in Mに対してb_2\succ bゆえ、強補間性よりb_2\succ b_1\succ b\text{ for all }\mathord\Downarrow{b}\in Mなるb_1\in Bが存在。
補間性

b_2\mathrel{\theta}\mathord\Downarrow{b_1}とすれば、b_2\succ b_1より、強補間性よりb_2\succ b_2'\succ b_1なるb_2'\in Bが存在。

\phi\circ\theta=\mathord\succについて\begin{array}{cll}
&& b_2\mathrel{\phi\circ\theta}b_0 \\
\iff & \exists b_1\in B, & b_2\mathrel{\theta}\mathord\Downarrow{b_1}\mathrel{\phi}b_0 \\
\iff & \exists b_1\in B, & b_2\succ b_1\succ b_0 \\
\iff && b_2\succ b_0
\end{array}
\theta\circ\phi=\mathord\ggについて\begin{array}{cll}
&& \mathord\Downarrow{b_2}\mathrel{\theta\circ\phi}\mathord\Downarrow{b_0} \\
\iff & \exists b_1\in B, & \mathord\Downarrow{b_2}\mathrel{\phi}b_1\mathrel{\theta}\mathord\Downarrow{b_0} \\
\iff & \exists b_1\in B, & b_2\succ b_1\succ b_0 \\
\iff && b_2\succ b_0 \\
\iff && \mathord\Downarrow{b_2}\gg\mathord\Downarrow{b_0}
\end{array}\square
!定理16は抽象基底が最小元を持たなくても、最小元を必ずしも持たないイデアル完備化から元の抽象基底が復元可能という意味で成り立ちます。
しかし、dcpoは最小元を持つという定義が一般的であり、その場合は定理16は最小元を持つ抽象基底に対してのみ成り立つことに注意してください。

（本記事でも原則dcpoは最小元を持つものとして話をしていますが、定理9や定理16ではあえて一般的な抽象基底でステートメントを述べました）
今、近似可能関係R\subseteq B\times Cからは連続写像f_R\colon\mathbf{RI}(B)\to\mathbf{RI}(C)が次のように得られます。

f_R(I)\coloneqq\bigcup\{R(b)\mid b\in I\}
連続性の証明
\begin{array}{ll}& \bigcup f(\mathcal A)\subseteq I_0\\
\iff&\forall I\in\mathcal A, f(I)\subseteq I_0\\
\iff&\forall I\in\mathcal A, \bigcup\{R(b)\mid b\in I\}\subseteq I_0\\
\iff&\forall I\in\mathcal A, \forall b\in I, R(b)\subseteq I_0\\
\iff&\forall b\in\bigcup\mathcal A, R(b)\subseteq I_0\\
\iff&\bigcup\{R(b)\mid b\in \bigcup\mathcal A\}\subseteq I_0\\
\iff&f(\bigcup\mathcal A)\subseteq I_0\end{array}
また、連続写像f\colon D\to Eに対し、D, Eからそれぞれ基底(B_D, \ll_D), (B_E, \ll_E)を取ると、近似可能関係R_f^{B_D, B_E}\subseteq B_D\times B_Eは次のように得られます。（approximable relationとなるのは連続性以外は定義より明らか。連続性は補題3-5より）

b\mathrel{R_f}c\iff c\ll_E f(b)
このとき、fとf_{R_f}、RとR_{f_R}は「一致」します。

 定理17: \beta, \thetaは自然同型連続dcpo D, Eに対し、基底B_D\subseteq D, B_E\subseteq Eを取る。そのとき、連続写像f\colon D\to Eは次を可換にする。

（\beta_Dは定理11における写像\beta_D(x)\coloneqq\{b\in B_D\mid b\ll x\}\colon D\to\mathbf{RI}(B_D)）

\begin{array}{ccc}
D & \xrightarrow{f} & E \\
\downarrow^{\beta_D} & & \downarrow^{\beta_E} \\
\mathbf{RI}(B_D) & \xrightarrow{f_{R_f}} & \mathbf{RI}(B_E)
\end{array}
抽象基底B, C間の近似可能関係R\subseteq B\times Cは次を可換にする。

（\theta_Bは定理16における近似可能関係\theta_B=\{(b_2, \mathord\Downarrow{b_1})\mid b_2\succ b_1\in B_D\}\colon B\to i[B]で、B_{\mathbf{RI}(B)}\coloneqq i[B]とする）

\begin{array}{ccc}
B & \xrightarrow{R} & C \\
\downarrow^{\theta_B} & & \downarrow^{\theta_{C}} \\
B_{\mathbf{RI}(B)} & \xrightarrow{R_{f_R}} & B_{\mathbf{RI}(C)}
\end{array}
証明1について任意のx\in Dに対し、B_E\cap\mathord\Downarrow{f(x)}=f_{R_f}(B_D\cap\mathord\Downarrow{x})を示す。
\begin{array}{cll}
& f_{R_f}(B_D\cap\mathord\Downarrow{x}) \\
= & \bigcup\{R_f(b)\mid b\in B_D\cap\mathord\Downarrow{x}\} \\
= & \{c\in B_E\mid\exists b\in B_D\cap\mathord\Downarrow{x}, c\ll f(b)\} \\
= & \{c\in B_E\mid c\ll f(x)\} \\
= & B_E\cap\mathord\Downarrow{f(x)}
\end{array}下から２つ目の等号は補題3-5を用いた。
2について任意の(b, \mathord\Downarrow{c})\in B\times i[C]に対し、b\mathrel{\theta_C\circ R}\mathord\Downarrow{c}\iff b\mathrel{R_{f_R}\circ\theta_B}\mathord\Downarrow{c}を示す。
\begin{array}{cll}
& b\mathrel{R_{f_R}\circ\theta_B}\mathord\Downarrow{c} & \\
\iff & \exists b_1\in B, b\mathrel{\theta_B}\mathord\Downarrow{b_1}\mathrel{R_{f_R}}\mathord\Downarrow{c} & \\
\iff & \exists b_1\in B, b\succ b_1\text{ and }\mathord\Downarrow{c}\ll f_R(\mathord\Downarrow{b_1}) & \\
\iff & \exists b_1\in B, b\succ b_1\text{ and }\mathord\Downarrow{c}\ll\bigcup\{R(b_2)\mid b_2\prec b_1\} & \\
\iff & \exists b_1\in B, b\succ b_1\text{ and }\exists b_2\prec b_1, \exists c'\in R(b_2), \mathord\Downarrow{c}\ll\mathord\Downarrow{c'} & (\because\text{lem. 8-6})\\
\iff & \exists b_2\in B, b\succ b_2\text{ and }\exists c'\in R(b_2), c\prec c' & (\because\text{trans \& SIP})\\
\iff & \exists c'\in R(b), c\prec c' & (\because\text{mono \& conti of }R)\\
\iff & \exists c'\in C, b\mathrel{R}c'\text{ and }c'\succ c \\
\iff & \exists c'\in C, b\mathrel{R}c'\mathrel{\theta_C}\mathord\Downarrow{c}\\
\iff & b\mathrel{\theta_C\circ R}\mathord\Downarrow{c}
\end{array}\square
これまで連続dcpoの基底を取る際、原則どの基底をを取るかは特に指定していませんでした。

しかし、定理16のみ抽象基底のイデアル完備化からはi[B]を取ることを指定しています。
何か標準的な取り方があればよいのですが、実は連続dcpo上の基底は全て同型であることが証明できます。

つまりどれを取っても変わらないということなので、連続dcpo (D, \le)に対して、以降ではB_D\coloneqq(D, \ll)と取ることに決めてしまいましょう。

 定理18: すべての基底は同型連続dcpo D上の任意の基底 B, C\subseteq Dを取る。

近似可能関係R\colon B\to C, S\colon C\to Bを次のように定める。
R=\{(b, c)\mid b\gg c\}\colon B\to C
S=\{(c, b)\mid c\gg b\}\colon C\to B
このとき、R\circ S=\mathord\gg及びS\circ R=\mathord\ggが成り立つ。

すなわち、Rは同型であり、(B, \ll)\cong(C, \ll)が成り立つ。
証明
R, Sは近似可能関係Rが近似可能関係であることを示す。（Sについても同様）
単調性

b_2\gg b_1\mathrel{R}cとすれば、推移性からb_2\gg cとなる。
下方性

b\mathrel{R}c_1\gg c_0とすれば、推移性からb\gg c_0となる。
有向性

b\mathrel{R}Mとすれば、b\gg Mゆえ、強補間性よりb\gg c\gg Mなるc\in Cが存在。
補間性

b_2\mathrel{R}\mathord cとすれば、b_2\gg cゆえ、強補間性よりb_2\gg b_1\gg cなるb_1\in Bが存在。

S\circ R=\mathord\ggについて\begin{array}{cll}
&& b_2\mathrel{S\circ R}b_1 \\
\iff & \exists c\in C, & b_2\mathrel{R}c\mathrel{S}b_1 \\
\iff & \exists c\in C, & b_2\gg c\gg b_1 \\
\iff && b_2\gg b_1
\end{array}
R\circ S=\mathord\ggについて\begin{array}{cll}
&& c_2\mathrel{R\circ S}c_1 \\
\iff & \exists b\in B, & c_2\mathrel{S}b\mathrel{R}c_1 \\
\iff & \exists b\in B, & c_2\gg b\gg c_1 \\
\iff && c_2\gg c_1 \\
\end{array}\square
改めて、連続dcpo Dに対し、標準的な基底の取り方としてB_D\coloneqq(D, \ll)と定めることにしましょう。
ここで、これまでの結果をまとめます。

D\cong\mathbf{RI}(B_D)（定理11）

B\cong B_{\mathbf{RI}(B)}（定理16）

fとf_{R_f}は「一致」する（定理17-1）

R_fとR_{f_R}は「一致」する（定理17-2）
これら結果を用いることで、詳細な定義は省きますが次が従います。

 定理19: 連続dcpoと抽象基底は圏同値連続dcpo及び連続写像からなる圏\mathbf{CONT}と最小元を持つ抽象基底及び近似可能関係からなる圏\mathbf{ABS}は圏同値である。
このようにして、我々は連続dcpoの表現を得ることができました。

また、ほとんど同様に以下の結果も得ることができます。

 定理20: 代数的dcpoとposetは圏同値代数的dcpo及び連続写像からなる圏\mathbf{ALG}と最小元を持つposet及び近似可能関係からなる圏\mathbf{POS}は圏同値である。
ちなみに、前順序集合 (P, \preceq)に対し、関係\mathord\sim\subseteq P\times Pをa\sim b\iff a\le b\land b\le aと定義すると、\mathord\simは同値関係となり、P/\mathord\simに対して[a]\le[b]\iff a\preceq b (well-defined)と定義した(P/\mathord\sim, \le)がposetとなることは有名ですが、実は近似可能関係の意味で(P/\mathord\sim, \le)と(P, \preceq)は同型になります。
つまり、近似可能関係による同一視のもとでは全ての前順序集合は一つのposetに吸収されることになるため前順序集合と近似可能関係による圏は\mathbf{POS}と圏同値になるため、定理20のステートメントは前順序にしても同じことが言えます。

 命題21: 前順序集合とposetの同型性前順序集合(P, \preceq)から得たposet (P/\mathord\sim, \le)は、近似可能関係の意味で(P, \preceq)と同型である。
証明 (sketch)R=\{(a, [b])\mid a\succeq b\in P\}\colon P\to P/\mathord\sim, S=\{([a], b)\mid a\succeq b\in P\}\colon P/\mathord\sim\to Pと定義する。 (wll-defined)
だいたい同じ流れでR, Sは近似可能関係となり、S\circ R=\mathord\succeq及びR\circ S=\mathord\geが成り立つことが言える。

\square
また、posetに限れば近似可能関係による同型と全単射な単調写像による同型は一致します。
近似可能関係による同型を\cong_\mathrm{app}とし、全単射な単調写像による同型を\cong_\mathrm{mono}とします。dcpo間の同型は\cong_\mathrm{conti}とします。

 命題22: posetの同型性poset P, Qに対し、P\cong_\mathrm{app}Q\iff P\cong_\mathrm{mono}Q
証明 (sketch)
\impliedbyについて全単射な単調写像をf\colon P\to Qとし、R=\{(a, f(b))\in P\times Q\mid a\ge_Pb\in P\}\colon P\to Q, S=\{(f(a), b)\in Q\times P\mid a\ge_Pb\in P\}\colon Q\to Pと定義する。
これもだいたい同じ流れでR, Sは近似可能関係となり、S\circ R=\mathord\ge_P及びR\circ S=\mathord\succeq_Qが成り立つことが言える。

\impliesについてまず、代数的dcpoがD\cong_\mathrm{conti}Eなとき、\mathcal{K}(D)\cong_\mathrm{mono}\mathcal{K}(E)が成り立つことを言う。

D, E間の全単射な連続写像をf\colon D\to Eとすれば、fの\mathcal K(D)への制限f'はf'\colon\mathcal K(D)\to\mathcal K(E)なる全単射な単調写像となることを言えばよい。

まず、E上の有向集合は常にあるD上の有向集合Aを用いてf[A]と表せる。また、(\forall A\subseteq_\mathrm{dir}D, c\le\sqcup A\implies\exists a\in A, c\le a)\iff(\forall A\subseteq_\mathrm{dir}D, f(c)\sqcup f[A]\implies\exists a\in f[A], f(c)\le a)も容易にわかるため、f'はf'\colon\mathcal K(D)\to\mathcal K(E)なる全単射な単調写像となる。
また、poset Pに対して、P\cong_\mathrm{mono}\mathcal{K}(\mathbf{RI}(P))も言える。これは、a\mapsto\mathord\downarrow{a}\colon P\to\mathbf{RI}(P)が明らかに全単射な単調写像となるため言える。
ゆえに、P\cong_\mathrm{app}Qのとき、\mathbf{RI}(P)\cong_\mathrm{conti}\mathbf{RI}(Q)ゆえ、P\cong_\mathrm{mono}\mathcal{K}(\mathbf{RI}(P))\cong_\mathrm{mono}\mathcal{K}(\mathbf{RI}(Q))\cong_\mathrm{mono}Qが成り立つ。
（つまり、直接的には同型R\colon P\to Qに対して、f_R\colon\mathbf{RI}(P)\to\mathbf{RI}(Q)のPへの制限f_R'として全単射な単調写像が得られる。）

\square
ゆえに、圏\mathbf{POS}は射として全単射な単調写像を用いても近似可能関係を用いたものと圏同値になるので、\mathbf{POS}を考える際は原則全単射な単調写像を用いることにしましょう。

 おわりにお疲れ様でした。ここまで読んでいただきありがとうございました。
抽象基底の理論は連続dcpoを扱う上で非常に重要かつ基本的な理論なため、多くの文献で紹介がされています。
しかし、本記事で示した近似可能関係に関する多くの命題は常識として省かれていることが多く、初学者には非常に取っ掛かりにくい分野になってしまっているように感じました。
特に、定理16, 17に関しては本当に大量の論文や教科書を漁ったものの詳細な証明どころか、詳細なステートメントを述べている文献すら一つも見つからなかったため、私自身で（\thetaの定義など）解釈して証明を試みてみました。

（まるで常識かのように扱っておいて、自分自身が全然理解しておらず大したリサーチも考察もせず嘘八百を載せてる論文も見ました）
そのため、本記事は日本語どころか英語含めてもほとんど初となるレベルの詳しさで抽象基底の超基礎的事項をまとめたものになっているという自負があります。
もしいつかこの記事が誰かの役に立てたらとても嬉しいです。
改めて、本当にありがとうございました。

脚注
Winskelの"The Formal Semantics of Programming Languages"（和訳：『プログラミング言語の形式的意味論入門』）ではapproximable mappingと呼ばれ近似可能写像と訳されていましたが、approximable relationと呼ぶのが一般的に感じたためここでは近似可能関係と訳しました。 ↩︎
抽象基底はM. B. Smythの"Effectively Given Domains"が初出であり、当初はR-structureと呼ばれていました。 ↩︎
イデアル完備化については私のBöhm木についての記事でもより丁寧にお気持ちを解説しています。 ↩︎
可算な台集合上の推移的関係のイデアル完備化はQuasi-Polish空間、すなわち、\omega-連続dcpoの\Pi^0_2-部分空間となることも有名です。 ↩︎
抽象基底が最小元を持つとき、またその場合に限りイデアル完備化は最小元を持ちます。 ↩︎
連続性を除いた三条件（場合によっては単調性と下方性がまとめられた二条件）を定義とするものを知っている方もいるかもしれませんが、それはおそらくposetに対する近似可能関係です。posetでは連続性は反射性より常に成り立ちます。 ↩︎
一般の関係R\subseteq A\times B, S\subseteq B\times Cの合成はS\circ R=\{(a, c)\in A\times C\mid \exists b\in B, (a, b)\in R\land (b, c)\in S\}と定義されます。 ↩︎