範疇論學習筆記19：伽羅瓦連接

05-03

目錄：類型論驛站寫作計劃

前一篇：範疇論學習筆記18：可表函子和普遍元素

後一篇：範疇論學習筆記20：伴隨

學習材料：Category Theory: A Gentle Introduction - Logic Matters，最近更新（2018年1月29日）的版本。這份筆記對應的是第 27 章。

伴隨（adjunction） 是範疇論中十分重要的一個概念。伽羅瓦連接（Galois connections）是一種特殊的伴隨，即兩個作為範疇的偏序集合之間的伴隨關係。Peter Smith 的教材A Gentle Introduction 一直都是從特殊到一般地引入範疇論里的重要概念的。

定義119（偏序集合之間的函數）

假設 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 是兩個偏序集合（posets）。設映射 $F:mathscr{C o D}$ 是載體集合（carrier sets） $C$ 和 $D$ 之間的函數。那麼

$F$ 是單調（monotone）的，只要 $forall x,yin C. xpreccurlyeq y Rightarrow Fxsqsubseteq Fy.$
$F$ 是序嵌入（order-embedding）的，只要 $forall x,yin C.xpreccurlyeq yiff Fx sqsubseteq Fy$ .
$F$ 是序同構（order-isomorphism）的，當且僅當 $F$ 是一個滿射的序嵌入。

針對上述定義，值得注意的是：

單調映射的複合也是單調映射；單調映射的複合滿足結合律
序嵌入是單射
如果 $F[C]$ 是 $C$ 在 $F$ 下的像，那麼序嵌入 $F:(C,preccurlyeq) o(D,sqsubseteq)$ 是一個從 $(C,preccurlyeq)$ 到 $(F[C],sqsubseteq)$ 的序同構
序同構是雙射，可以視為集合函數的同構。序同構有唯一的逆（inverse），這個逆也是序同構
如果偏序集合之間存在序同構，那麼它們被認為是同構的

定義120

設 $Pi$ 是一個集合的搜集（collection）。那麼以包含關係（inclusion）排序的 $Pi$ ，即 $(Pi,subseteq)$ ，是一個包含偏序集合（inclusion poset）。

定理148

每一個偏序集合都和一個包含偏序集合同構。

句法語義之間的連接

設有形式語言 $mathcal{L}$ ，我們有一個偏序集合 $mathscr{C}=(C,preccurlyeq)$ ， $C$ 的成員是句子的集合。 $preccurlyeq$ 就是普通的集合包含關係。因此， $C$ 的成員可以視為用 $mathcal{L}$ 表述的理論（theories）。這些理論從一般到具體有著部分排序。

又有一個對應的偏序集合 $mathscr{D}=(D,sqsubseteq)$ ， $D$ 的成員是 $mathcal{L}$ 結構，即相應理論的可能的模型的集合，的搜集。我們將 $sqsubseteq$ 視為包含的逆關係。 $D$ 的成員可以視為使得理論正確的可能世界模型組成的集合。這個可能世界模型的集合也是按從一般（更多可能性）到具體（更少的可能世界模型選擇）來排序的。

那麼，在這兩個偏序集合之間，存在著兩個非常自然的映射：

$F:mathscr{C o D}$ 將理論 $cin C$ 映射到滿足理論的模型的集合 $din D$ （找模型函數）
$G:mathscr{D o C}$ 將模型集合 $din D$ 映射到在 $d$ 的每一個模型中都為真的句子的集合 $c$ 上（找句子函數）

我們有如下觀察：

$F$ 和 $G$ 是單調的
$forall cin C.forall din D. cpreccurlyeq GFc wedge FGdsqsubseteq d$
$forall c in C. d in D. Fc sqsubseteq d iff c preccurlyeq Gd$
$FGF=F, GFG= G$

伽羅瓦連接的定義

定義121

假設 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 是兩個偏序集合，設映射 $F:mathscr{C o D}$ 和 $G:mathscr{D o C}$ 是一對函數，使得對於所有 $cin C, din D$ ,

$(G)phantom{some} Fcsqsubseteq d iff c preccurlyeq Gd$

那麼 $F$ 和 $G$ 就構成了一個 $mathscr{C}$ 和 $mathscr{D}$ 之間的伽羅瓦連接，記作 $Fdashv G$ ，我們稱 $F$ 是 $G$ 左伴隨（left adjoint）， $G$ 被稱為 $F$ 的右伴隨（right adjoint）。

除了上面的例子之外，伽羅瓦連接的例子還包括：

設 $F$ 為 $(C,preccurlyeq)$ 和 $(D,sqsubseteq)$ 之間的序同構，那麼 $F^{-1}$ 是一個反方向的序同構。取 $cin C,din D$ ，那麼平凡地， $Fdashv F^{-1}$
取 $mathscr{N}=(mathbb{N},le), mathscr{Q}^{+}(mathbb{Q}^+,le)$ ，設 $I:mathscr{N o Q^+}$ 是從自然數到相應的有理數的單射函數，設 $F:mathscr{Q^+ o N}$ 是取底函數。那麼 $Idashv F$ 是一個伽羅瓦連接。設 $C$ 為取頂函數，那麼 $Cdashv I$ 是反方向的伽羅瓦連接。
選取邏輯證明系統 $mathcal{L}$ ，設 $alphavdash eta$ 指代從前提 $alpha$ 到結論 $eta$ 之間存在一個形式證明。使 $|alpha|$ 為該系統里和 $alpha$ 等價的一類合式公式（wffs）。取 $E$ 作為這些等價類的集合，設定在 $E$ 中 $|alpha|preccurlyeq |eta|iff alphavdash eta$ 。那麼 $(E,preccurlyeq)$ 是一個偏序集合。使 $gamma$ 為固定的合式公式。設 $F(|alpha|)=|(gamma wedge alpha)|, G(|alpha|)=|(gamma o alpha)|$ 。根據正規性假設，我們有 $gammawedge alphavdash eta iff alphavdash gamma o eta$ ，所以 $F|alpha|preccurlyeq |eta| iff |alpha|preccurlyeq G|eta|$ 。所以 $(E,preccurlyeq)$ 和它自己之間存在一個伽羅瓦連接 $Fvdash G$ 。
上面的例子告訴我們「合取是條件式化的左伴隨」（conjunction is left adjoint to conditionalization）。
選取一階邏輯證明系統 $mathcal{L}$ ，取最有變數 $vec{x}$ 是自由的 $mathcal{L}$ 合式公式的集合。我們將這類公式寫作 $varphi(vec{x})$ ，其等價類寫作 $|varphi(vec{x})|$ ，等價類的集合寫作 $E_{vec{x}}$ . $|alpha|preccurlyeq |eta|iff alphavdash eta$ . 考慮兩個偏序集合 $(E_{vec{x}},le), (E_{vec{x},y},le)$ 之間的映射。平凡映射 $F(|varphi(vec{x})|) = |varphi(vec{x})|$ ，量詞引入映射 $G(|varphi(vec{x},y)|) = |forall y. varphi(vec{x},y)|$ 。那麼 $Fdashv G$ 是一個伽羅瓦連接： $F(|varphi(vec{x})|)preccurlyeq|psi(vec{x},y)|iff |varphi(vec{x})|preccurlyeq G(|psi(vec{x},y)|)$ ，反映的恰恰是我們所熟知的邏輯法則 $varphi(vec{x})vdash psi(vec{x},y)iff varphi(vec{x})vdash forall y.psi(vec{x},y)$ ，只要 $y$ 在 $varphi(vec{x})$ 中不自由出現。
由上可知，全稱量化（universal quantification）是特定的平凡包含運算的右伴隨。同樣地，我們可以推出，存在量化（existential quantification）是同樣運算的左伴隨。

定理149

假設 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 是兩個偏序集合（posets）。設映射 $F:mathscr{C o D}$ 是載體集合（carrier sets） $C$ 和 $D$ 之間的函數。那麼 $Fdashv G$ 當且僅當

$F$ 和 $G$ 是單調的
$forall cin C.forall din D. cpreccurlyeq GFc wedge FGdsqsubseteq d$
$FGF=F, GFG= G$

定義122（伽羅瓦連接的重新定義）

假設 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 是兩個偏序集合（posets）。設映射 $F:mathscr{C o D}$ 是載體集合（carrier sets） $C$ 和 $D$ 之間的函數。如果對於所有的 $cin C,din D$ ,

$F$ 和 $G$ 是單調的
$cpreccurlyeq GFc wedge FGdsqsubseteq d$
$FGF=F, GFG= G$

那麼 $F$ 和 $G$ 構成了一個 $mathscr{C}$ 和 $mathscr{D}$ 之間的伽羅瓦連接。

伽羅瓦連接的一些基本結論

定理150（傳遞性）

假設偏序集合 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 之間存在著一個伽羅瓦連接 $Fdashv G$ ， $mathscr{D}$ 和偏序集合 $mathscr{E}=(E,subseteq)$ 之間存在著一個伽羅瓦連接 $Hdashv K$ 。那麼 $mathscr{C}$ 和 $mathscr{E}$ 之間存在著一個伽羅瓦連接 $HFdashv GK$ 。

定理151（唯一性）

如果偏序集合 $mathscr{C}=(C,preccurlyeq )$ 和 $mathscr{D}=(D,sqsubseteq)$ 之間存在著伽羅瓦連接 $Fdashv G,Fdashv G$ ，那麼 $G=G$ 。同樣地，如果它們之間存在著伽羅瓦連接 $Fdashv G,Fdashv G$ ，那麼 $F=F$ 。