Steve Awodey の Category Theory を読む : Chapter 6

Steve Awodey の Category Theory を読むシリーズトップ

6.2 Cartesian closed categories
- Example 6.5
- Example 6.6
6.3 Heyting Algebras
- Definition 6.10
6.7 Variable sets
- Exercise 15(a)
- Exercise 15(b)
参考書籍

6.2 Cartesian closed categories

Example 6.5

$\omega$ CPO はプログラミング言語の Denotational Semantics で使用される重要な代数構造なのでここでは詳しく証明しておきます。

$Q^{P}$ is an $\omega$ CPO

任意の $f_{0} \leq f_{1} \leq \cdots$ に対して、 $\varinjlim_{i} f_{i}$ を任意の $p \in P$ に対して $\left( \varinjlim_{i} f_{i} \right)(p) = \varinjlim_{i} f_{i}(p)$ で定義します。この $\varinjlim_{i} f_{i}$ が monotone かつ $\omega$ -continuous であることを証明します。

$Lemma$
$\varinjlim_{i} f_{i} \text{ is monotone}.$

$Proof.$
任意の $p, p' \in P$ と任意の $i \in N$ に対して、 $f_{i}$ が monotone であることより、 $f_{i}(p) \leq f_{i}(p') \leq \varinjlim_{i} f_{i}(p')$ が成り立つ。よって colimit の UMP より $\left( \varinjlim_{i} f_{i} \right)(p) = \varinjlim_{i} f_{i}(p) \leq \varinjlim_{i} f_{i}(p') = \left( \varinjlim_{i} f_{i} \right)(p')$ が成り立つ。

$\square$

次に $\varinjlim_{i} f_{i}$ が $\omega$ -continuous であることを証明するのですが、その前に準備として任意の $f_{0} \leq f_{1} \leq \cdots$ と任意の $p_{0} \leq p_{1} \leq \cdots$ に関して次の事柄を証明しておきます。

$Lemma$
$\exists \varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots ,\, \exists \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) ,\, \forall i,\, \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)$

$Proof.$
任意の $i$ に対して $\varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{j} f_{i+1}(p_{j})$ を示せば、 $\varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots$ が $\omega$ chain となる。すると $Q$ が $\omega$ CPO であることから残りの性質は明らかである。
$f_{i}, f_{i+1}$ が $\omega$ -continuous であることから、 $f_{i}(\varinjlim_{j} p_{j}) \leq f_{i+1}(\varinjlim_{j} p_{j})$ を示せばよいが、 $f_{i} \leq f_{i+1}$ であるからこれは成り立つ。

$\square$

$Lemma$
$\exists \varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots ,\, \exists \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) ,\, \forall j,\, \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$

$Proof.$
任意の $j$ に対して $\varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{j+1})$ を示せば、 $\varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots$ が $\omega$ chain となる。すると $Q$ が $\omega$ CPO であることから残りの性質は明らかである。
$\varinjlim_{i} f_{i}$ が monotone であることより $\varinjlim_{i} f_{i}(p_{j}) = \left( \varinjlim_{i} f_{i} \right) (p_{j}) \leq \left( \varinjlim_{i} f_{i} \right) (p_{j+1}) = \varinjlim_{i} f_{i}(p_{j+1})$ が成り立つ。

$\square$

$Lemma$
$\varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) = \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$

$Proof.$

$\varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$

任意の $i$ と任意の $j$ に対して $f_{i} \leq \varinjlim_{i} f_{i}$ と上で示したことより $f_{i}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$ が成り立つ。
すると $\omega$ chain $f_{i}(p_{0}) \leq f_{i}(p_{1}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$ が成り立つ。
さらに上で示した $\omega$ chain $\varinjlim_{j} f_{0}(p_{j}) \leq \varinjlim_{j} f_{1}(p_{j}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \leq \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right)$ が成り立つ。

$\varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)$

任意の $j$ と任意の $i$ に対して $f_{i}$ が monotone であることと上で示したことより $f_{i}(p_{j}) \leq \varinjlim_{j} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)$ が成り立つ。
すると $\omega$ chain $f_{0}(p_{j}) \leq f_{1}(p_{j}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{i} f_{i}(p_{j}) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)$ が成り立つ。
さらに上で示した $\omega$ chain $\varinjlim_{i} f_{i}(p_{0}) \leq \varinjlim_{i} f_{i}(p_{1}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \leq \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right)$ が成り立つ。

$\square$

以上の準備を元に $\varinjlim_{i} f_{i}$ が $\omega$ -continuous であることを証明します。

$Lemma$
$\varinjlim_{i} f_{i} \text{ is } \omega \text{-continuous}.$

$Proof.$
\begin{align*}
\left( \varinjlim_{i} f_{i} \right) (\varinjlim_{j} p_{j}) &\underset{\text{def}}{=} \varinjlim_{i} f_{i} \left( \varinjlim_{j} p_{j} \right) \\
&\underset{f_{i} \text{ is continuous}}{=} \varinjlim_{i} \left( \varinjlim_{j} f_{i}(p_{j}) \right) \\
&= \varinjlim_{j} \left( \varinjlim_{i} f_{i}(p_{j}) \right) \\
&\underset{\text{def}}{=} \varinjlim_{j} \left( \left( \varinjlim_{i} f_{i} \right) (p_{j}) \right)
\end{align*}

$\square$

$\epsilon$ is $\omega$ -continuous

まず任意の $\omega$ chain $(f_{0}, p_{0}) \leq (f_{1}, p_{1}) \leq \cdots$ に関して以下の事柄を証明します。

$Lemma$
$\varinjlim_{i} (f_{i}, p_{i}) = \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right)$

$Proof.$
任意の $i$ に対して $f_{i} \leq \varinjlim_{j} f_{j}$ かつ $p_{i} \leq \varinjlim_{k} p_{k}$ が成り立つ。よって $(f_{i}, p_{i}) \leq \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right)$ が成り立つ。
任意の $(x,y)$ と任意の $i$ に対して $(f_{i}, p_{i}) \leq (x, y)$ が成り立つとする。すると $\omega$ chain $f_{0} \leq f_{1} \leq \cdots$ に対する colimit の UMP より $\varinjlim_{j} f_{j} \leq x$ が成り立つ。同様に $\varinjlim_{k} p_{k} \leq y$ が成り立つ。よって $\left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right) \leq (x, y)$ が成り立つので、 $\varinjlim_{i} (f_{i}, p_{i}) = \left( \varinjlim_{j} f_{j}, \varinjlim_{k} p_{k} \right)$ である。

$\square$

$Lemma$
$\epsilon \left( \varinjlim_{i} (f_{i}, p_{i}) \right) = \varinjlim_{i} \epsilon( f_{i}, p_{i})$

$Proof.$
上で証明したことと $\epsilon$ の定義より、証明するべきことは $\left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) = \varinjlim_{i} f_{i}(p_{i})$ である。

$\varinjlim_{i} f_{i}(p_{i}) \leq \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right)$

任意の $i$ に対して、

\begin{align*}
f_{i}(p_{i}) &\underset{f_{i} \text{ is monotone}}{\leq} f_{i} \left( \varinjlim_{k} p_{k} \right) \\
&\leq \varinjlim_{j} \left( f_{j} \left( \varinjlim_{k} p_{k} \right) \right) \\
&\underset{\text{def}}{=} \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right)
\end{align*}

$\omega$ chain $f_{0}(p_{0}) \leq f_{1}(p_{1}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{i} f_{i}(p_{i}) \leq \left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right)$ が成り立つ。

$\left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i})$

任意の $j$ と任意の $k$ に対して、 $f_{j} (p_{k}) \leq \varinjlim_{i} f_{i}(p_{i})$ を示す。
$j \leq k$ のとき、
$f_{j}(p_{k}) \leq f_{k}(p_{k}) \leq \varinjlim_{i} f_{i}(p_{i})$ が成り立つ。
$k \leq j$ のとき、
$f_{j}(p_{k}) \leq f_{j}(p_{j}) \leq \varinjlim_{i} f_{i}(p_{i})$ が成り立つ。
よって $\omega$ chain $f_{j}(p_{0}) \leq f_{j}(p_{1}) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{k} f_{j}(p_{k}) \leq \varinjlim_{i} f_{i}(p_{i})$ が成り立つ。これは $f_{j}$ が continuous であることより $f_{j} \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i})$ と同値である。
すると $\omega$ chain $f_{0} \left( \varinjlim_{k} p_{k} \right) \leq f_{1} \left( \varinjlim_{k} p_{k} \right) \leq \cdots$ に対する colimit の UMP より $\varinjlim_{j} f_{j} \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i})$ が成り立つ。定義より $\left( \varinjlim_{j} f_{j} \right) \left( \varinjlim_{k} p_{k} \right) \leq \varinjlim_{i} f_{i}(p_{i})$ である。

$\square$

$\tilde{f}$ is $\omega$ -continuous if $f$ is so

任意の $\omega$ chain $x_{0} \leq x_{1} \leq \cdots$ に対して、以下の事柄を証明します。

$Lemma$
$\tilde{f} \left( \varinjlim_{i} x_{i} \right) = \varinjlim_{i} \tilde{f}(x_{i})$

$Proof.$
任意の $p \in P$ に対して $\tilde{f} \left( \varinjlim_{i} x_{i} \right)(p) = \left( \varinjlim_{i} \tilde{f}(x_{i}) \right)(p)$ を示せばよいが、これは $\tilde{f}$ の定義より $f \left( \varinjlim_{i} x_{i}, p \right) = \varinjlim_{i} f(x_{i}, p)$ と同値である。
$\omega$ chain $(x_{0},p) \leq (x_{1}, p) \leq \cdots$ に対して、上で証明したことより $\varinjlim_{i} (x_{i}, p) = \left( \varinjlim_{i} x_{i}, p \right)$ が成り立つ。
よって $f$ が $\omega$ -continuous であることより $f \left( \varinjlim_{i} x_{i}, p \right) = f \left( \varinjlim_{i} (x_{i}, p) \right) = \varinjlim_{i} f(x_{i}, p)$ が成り立つ。

$\square$

Example 6.6

初めにテキストの通りに定義された $\epsilon$ が graph homomorphism であることを証明します。

$Lemma$
$\epsilon \colon H^{G} \times G \to H \text{ is a graph homomorphism}.$

$Proof.$
f:id:hitotakuchan:20160516120426p:plain
上の diagram が可換になることを示せばよい。
任意の $\theta \colon \phi \to \psi \in {H^{G}}_{e}$ と任意の $e \in G_{e}$ に対して、 $(s \circ \epsilon_{e})(\theta, e) = s(\theta(e)) = \phi(s(e))$ が成り立つ。さらに、 $(\epsilon_{v} \circ s)(\theta, e) = \epsilon_{v}(s(\theta), s(e)) = \epsilon_{v}(\phi, s(e)) = \phi(s(e))$ が成り立つ。よって $s \circ \epsilon_{e} = \epsilon_{v} \circ s$ が成り立つ。
同様に $t \circ \epsilon_{e} = \epsilon_{v} \circ t$ が成り立つ。

$\square$

次に $H^{G}$ が exponential object in $\bf{Graphs}$ であることを証明します。

$Lemma$
$H^{G} \text{ is an exponential object in } \bf{Graphs}.$

$Proof.$
初めに、任意の $f \colon F \times G \to H$ に対してテキストの通りに定義される $\tilde{f} \colon F \to H^{G}$ が graph homomorphism となることを証明する。それには次の diagram が可換となることを示せばよい。
f:id:hitotakuchan:20160516122209p:plain
これは任意の $c \colon a \to b \in F_{e}$ に対して、 $\tilde{f}_{e}(c) \colon \tilde{f}_{v}(a) \to \tilde{f}_{v}(b) \colon \in H^{G}_{e}$ となることと同値であり、さらに $H^{G}$ の定義より以下の diagram が可換になることと同値である。
f:id:hitotakuchan:20160516123743p:plain
任意の $e \in G_{e}$ に対して、 $\left( s \circ \tilde{f}_{e}(c) \right)(e) = s(f_{e}(c,e)) = f_{v}(s(c,e)) = f_{v}(a,s(e)) = \left( \tilde{f}_{v}(a) \right)(s(e)) = \left( \tilde{f}_{v}(a) \circ s \right)(e)$ が成り立つ。同様に $\left( t \circ \tilde{f}_{e}(c) \right)(e) = \left( \tilde{f}_{v}(b) \circ t \right)(e)$ が成り立つ。よって $\tilde{f}$ は graph homomorphism である。
この $\tilde{f}$ に対して $\epsilon \circ \left( \tilde{f} \times 1 \right) = f$ が成り立つことは明らかである。
次に任意の $f' \colon F \to H^{G}$ が $\epsilon \circ (f' \times 1) = f$ を満たすとする。
任意の $a \in F_{v}$ と任意の $u \in G_{v}$ に対して $f'_{v}(a)(u) = (\epsilon \circ (f' \times 1))(a, u) = f_{v}(a, u) = \tilde{f}_{v}(a)(u)$ が成り立つ。
また、任意の $c \in F_{e}$ と任意の $e \in G_{e}$ に対して $f'_{e}(c)(e) = (\epsilon \circ (f' \times 1))(c, e) = f_{e}(c, e) = \tilde{f}_{e}(c)(e)$ が成り立つ。よって $f' = \tilde{f}$ が成り立つ。

$\square$

6.3 Heyting Algebras

Definition 6.10

lattice に関しては complete であることと cocomplete であることが同値であることを証明します。
さらっと書かれていますが、その前の poset $P$ がすべての set-indexed meets を持てば、圏論的な意味で complete となるということの証明はできますか？
set-indexed meets を持つというのは、任意の集合 $I$ を離散圏とみなした場合に任意の diagram $D \colon I \to P$ が limit を持つことと言い換えられます。一方で、圏論的な意味で complete になるためには任意の diagram に対して limit を持たないといけません。
poset を圏とみなした場合、任意の対象間にはただ一つしか arrow が存在しないということから証明できます。

$Lemma$
$\text{A lattice } (L, \leq) \text{ is complete} \Rightarrow (L, \leq) \text{ is cocomplete}.$

$Proof.$
任意の $I$ -index 集合 $\left\{ a_{i} \in L \right\}$ に対して、集合 $I'$ を $I' = \left\{ b \in L \, \middle| \, \forall i \in I,\, a_{i} \leq b \right\}$ で定義する。すると、 $L$ が complete であることから、 $I'$ の limit $\bigwedge_{b \in I'} b$ が存在する。これが $\left\{ a_{i} \right\}$ の colimit $\bigvee_{i \in I} a_{i}$ であることを示す。
任意の $i \in I$ と任意の $b \in I'$ に対して $I'$ の定義より $a_{i} \leq b$ が成り立つ。すると、 $\bigwedge_{b \in I'} b$ は $I'$ の limit であるから limit の UMP より $a_{i} \leq \bigwedge_{b \in I'} b$ が成り立つ。
次に、任意の $x \in L$ が任意の $i \in I$ に対して $a_{i} \leq x$ を満たすとする。すると $I'$ の定義より $x \in I'$ が成り立つ。よって limit の定義より $\bigwedge_{b \in I'} b \leq x$ が成り立つ。
poset の anti-symmetricity より $\bigvee_{i \in I} a_{i} = \bigwedge_{b \in I'} b$ である。

$\square$

6.7 Variable sets

6.7.1 において証明が省略されている事柄は exercise 15 としてまとめられているので、そちらの証明をしておきます。

Exercise 15(a)

$Lemma$
${\bf{2}}^{I} \text{ is a Heyting algebra}.$

$Proof.$

${\bf{2}}^{I}$ has a terminal object $1$

$1$ を任意の $i \in I$ に対して $1(i) = \top$ で定義すると、任意の $f \in {\bf{2}}^{I}$ と任意の $i \in I$ に対して、 $f(i) \leq 1(i)$ が成り立つので $f \leq 1$ が成り立つ。

${\bf{2}}^{I}$ has products

任意の $f,g \in {\bf{2}}^{I}$ に対して $f \land g$ を任意の $i \in I$ に対して $(f \land g)(i) = f(i) \land g(i)$ で定義する。すると $f \land g \leq f$ かつ $f \land g \leq g$ が成り立つ。このとき $f \land g$ が product となることを示す。
任意の $h \in {\bf{2}}^{I}$ に対して $h \leq f$ かつ $h \leq g$ が成り立つとすると、任意の $i \in I$ に対して $h(i) \leq f(i) \land g(i)$ が成り立つので、 $h \leq f \land g$ が成り立つ。 ${\bf{2}}^{I}$ が poset であることより、これはただ一つに決まる。

${\bf{2}}^{I}$ has an initial object $0$

$0$ を任意の $i \in I$ に対して $0(i) = \bot$ で定義すれば、任意の $f \in {\bf{2}}^{I}$ に対して $0 \leq f$ が成り立つ。

${\bf{2}}^{I}$ has coproducts

任意の $f,g \in {\bf{2}}^{I}$ に対して $f \lor g$ を任意の $i \in I$ に対して $(f \lor g)(i) = f(i) \lor g(i)$ で定義する。すると product の場合と同様に $f \lor g$ は coproduct となる。

${\bf{2}}^{I}$ has exponentials

任意の $f, g \in {\bf{2}}^{I}$ に対して $f \Rightarrow g$ を任意の $i \in I$ に対して $(f \Rightarrow g)(i) = \top \iff \forall j \leq i,\, f(j) \leq g(j)$ で定義する。

$f \land g \leq h$ ならば $f \leq g \Rightarrow h$ が成り立つこと。
任意の $i \in I$ に対して $f(i) \leq (g \Rightarrow h)(i)$ を示せばよい。 $f(i) = \bot$ ならば $f(i) \leq (g \Rightarrow h)(i)$ は明らかである。 $f(i) = \top$ とすると、任意の $j \geq i$ に対して $g(j) \leq h(j)$ を示せばよいが、仮定より $f(j) \land g(j) \leq h(j)$ が成り立つ。また $f$ が monotone であることより $f(j) = \top$ が成り立つ。よって $g(j) \leq h(j)$ が成り立つ。

$f \leq g \Rightarrow h$ ならば $f \land g \leq h$ が成り立つこと。
任意の $i \in I$ に対して $f(i) \land g(i) \leq h(i)$ を示せばよい。 $f(i) = \bot$ ならば $f(i) \land g(i) \leq h(i)$ は明らかである。 $f(i) = \top$ とすると $g(i) \leq h(i)$ が成り立つことを示せばよい。仮定より $f(i) \leq g(i) \Rightarrow h(i)$ が成り立つが、 $f(i) = \top$ より $g(i) \Rightarrow h(i) = \top$ である。よって exponential の定義より $g(i) \leq h(i)$ が成り立つ。

$\square$

Exercise 15(b)

$Lemma$
$y(a) \text{ is monotone}.$

$Proof.$
任意の $x \leq y \in A^{op}$ に対して $y(a)(x) \leq y(a)(y) \in {\bf{2}}$ を示せばよい。 $y(a)(x) = \top$ の場合を考えれば十分である。このとき $x \leq a \in A$ が成り立つ。また $x \leq y \in A^{op}$ ならば $y \leq x \in A$ が成り立つので $y \leq a \in A$ が成り立つ。よって $y(a)(y) = \top$ となるので $y(a)(x) \leq y(a)(y)$ が成り立つ。

$\square$

$Lemma$
$y \text{ is monotone}.$

$Proof.$
任意の $a \leq b \in A$ に対して $y(a) \leq y(b) \in {\bf{2}}^{I}$ を示す。任意の $x \in A^{op}$ に対して $y(a)(x) = \top$ とすると $x \leq a \in A$ が成り立つ。 $a \leq b \in A$ より $x \leq b \in A$ が成り立つので $y(b)(x) = \top$ となる。よって $y(a) \leq y(b) \in {\bf{2}}^{I}$ が成り立つ。

$\square$

$Lemma$
$y \text{ is injective}.$

$Proof.$
任意の $a,b \in A$ に対して $y(a) = y(b)$ が成り立つとする。このとき任意の $x \in A^{op}$ に対して $y(a)(x) = y(b)(x)$ が成り立つ。 $x = a$ とすると $y(a)(a) = \top$ より $y(b)(a) = \top$ が成り立ち $a \leq b \in A$ が成り立つ。同様に $x = b$ とすると $b \leq a \in A$ が成り立つので $a = b$ となる。

$\square$

$Lemma$
$y \text{ preserves CCC structure}.$

$Proof.$

preserves terminal object $1$

任意の $x \in A^{op}$ に対して $y(1)(x) = \top$ が成り立つので $y(1) = 1 \in {\bf{2}}^{I}$ である。

preserves products

任意の $a,b \in A$ と任意の $x \in A^{op}$ に対して $y(a \land b)(x) = \left( y(a) \land y(b) \right)(x)$ を示せばよい。つまり $x \leq a \land b \iff x \leq a \land x \leq b \in A$ を示せばよいが、これは $a \land b$ が product であることより明らかである。

preserves exponentials

任意の $a,b \in A$ と任意の $x \in A^{op}$ に対して $y(a \Rightarrow b)(x) = \left( y(a) \Rightarrow y(b) \right)(x)$ を示せばよい。つまり $x \leq a \Rightarrow b \iff \forall y \geq x \in A^{op},\, y(a)(y) \leq y(b)(y)$ を示せばよい。

only if case
$y \leq a \in A$ とすると $x \leq y \in A^{op}$ より $y \leq x \in A$ であるから、 $y \leq x \land a$ が成り立つ。一方、仮定より $x \leq a \Rightarrow b$ であるから $x \land a \leq b$ が成り立つ。よって $y \leq b \in A$ となるので $y(a)(y) \leq y(b)(y)$ が成り立つ。

if case
$x \land a \leq x \in A$ が成り立つことから $x \leq x \land a \in A^{op}$ が成り立つ。すると仮定より $y(a)(x \land a) \leq y(b)(x \land a)$ が成り立つ。 $x \land a \leq a \in A$ は常に成り立つので、 $y(a)(x \land a) = \top$ となるから $y(b)(x \land a) = \top$ つまり $x \land a \leq b \in A$ が成り立つ。よって $x \leq a \Rightarrow b$ が成り立つ。