由伴隨函子生出單子 — From Adjoint Functors to Monads

「一對伴隨函子 (adjoint functor) 可以生出單子 (monad)」對一些人來說是「民眾知識」等級的東西 — 好像大家都知道,問出處則說不上來。因為最近的一些研究,我得把相關知識整理一下,順便註記於此。

伴隨函子

給定範疇 CD,與兩個函子(functor) L : C → DR : D → C. 如果給任何 C 之中的物件(object) AD 之中的物件 B,以下的自然同構均成立:

  Hom (L A, B) ≅ Hom (A, R B)

我們便說 LR 是一對伴隨函子 (adjoint functor) ,記為 L ⊣ R。其中 LR 分別稱為左伴隨 (left adjoint) 與右伴隨 (right adjoint)。

我們等下會解釋 Hom (A, B) 與自然同構等等概念。目前可暫時理解成:Hom (A, B) 是由 AB 的所有態射 (morphism)。如果考慮 Set 範疇,Hom (A, B) 是所有 A → B 的函數。因此 Hom (L A, B) ≅ Hom (A, R B) 可以理解為

  L A → B ≅ A → R B

意即:給任一個型別為 L A → B 的函數,我們可做出唯一一個 A → R(B) 的函數,反之亦然。一個例子是當 L A = A × S, R B = S → B,確實我們有

  (A × S) → B ≅ A → (S → B)

由左到右的對應便是 curry, 反過來的對應則是 uncurry.

Set 中的解釋只是(對我來說較好理解的)特例。各種範疇中,伴隨函子的例子相當多。例如,當考慮的範疇是偏序集合(partially ordered set 或 POSet,以偏序為態射),伴隨函子的意思便是 LR 形成一組 Galois connection.

「同構」意指存在一組函數:ϕ : Hom (L A, B) → Hom (A, R B)θ : Hom (A , R B) → Hom (L A, B), 滿足 ϕ ∘ θ = id θ ∘ ϕ = id,如同前述的 curryuncurry。「自然同構」要求 ϕθ 對於 AB 必須是自然變換 (natural transformation). 它們的自然轉換性質複雜但重要,我們後面會解釋並用到。

單子與餘單子

如果 L : C → DR : D → C 是一對伴隨函子, R ∘ L 是一個單子,L ∘ R 則是一個餘單子(comonad)。

以前述的 L A = A × S, R B = S → B 為例,(R ∘ L) A = S → (A × S) — 確實,這是狀態單子(state monad)的型別!

光有型別還不夠,還得有單子的操作才行。單子有兩種定義方式,在程式員常用的定義中,一個單子 M : * → * 附帶兩個運算子 return : A → M A(>>=) : M A → (A → M B) → M B。在數學圈比較常用的定義中,單子該有 return, map : (A → B) → M A → M B, 與 join : M (M A) → M A 三個運算子。在數學圈子的習慣中,returnjoin 分別寫做 ημ. 相對地,餘單子 N 也有三個運算元:ε : N B -> B, map : (A → B) → N A → N B, 與 δ : N B → N (N B).

如前所述,伴隨函子 LR 可衍生出單子 M = R ∘ L 與餘單子 N = L ∘ R。它們的 ηε 可分別定義為:

  η : A → R (L A)
  η = ϕ id      -- id 的 type 為 L A → L A

  ε : L (R B) → B
  ε = θ id       -- id 的 type 為 R B → R B

其中兩個 id 的型別如註解;μδ 則可定義為:

  μ : R (L (R (L A))) → R (L A)
  μ = R ε        -- ε 的 type 中,B := L A

  δ : L (R B) → L (R (L (R B)))
  δ = L η        -- η 的 type 中,A := R B

其中 η : R B → R (L (R B)), ε : L (R (L A)) → L A.

我們可自行檢查這幾個運算子的型別確實正確。但,它們是否滿足單子該有的條件?單子 (M, η, μ) 的規則有六條:

  1. M id = id
  2. M f ∘ M g = M (f ∘ g)
  3. η ∘ f = M f ∘ η
  4. M f ∘ μ = μ ∘ M (M f)
  5. μ ∘ η = id = μ ∘ M η
  6. μ ∘ μ = μ ∘ M μ

第 1, 2 條要求 M 是一個函子。由於 LR 均為函子,這兩條也立刻成立。第 3, 4 條要求 ημ 是自然變換,第 5, 6 條則和單子的計算比較相關。他們是否真的成立呢?

態射集合與態射函子

先回顧一下相關知識:給定範疇 CD,他們之間的一個函子(functor) F : C → DC 之中的物件(object) A 對應到 D 之中的物件 F A,並將 C 之中的態射(morphism) f : A → B 對應到 D 之中的態射 F f : F A → F B. 函子應滿足以下的函子規則

  F id = id
  F f ∘ F g = F (f ∘ g)

為了證明剩下的四條單子性質,我們看看有哪些關於 ϕθ 的性質可用。而為此,我們回頭看看之前提及,但迅速帶過的態射集合、自然同構等概念。

給定範疇 C 中的兩個物件 AB, 他們之間所有的態射記為 Hom(A,B). (一般說來 Hom(A,B) 不見得是集合。如果它是集合,C 被稱作一個局部小範疇 (locally small category).)(詳見 hom-set on ncatlab)

給定範疇 CHom 也是一個 Cᵒᵖ × C → Set 的函子(其中 CᵒᵖC 的逆範疇)。它將物件 Cᵒᵖ × C 中的物件 (c,d) 對應到前述的 Hom(A,B), 將一對態射 f : A₂ → A₁g : B₁ → B₂ 對應到一個態射 Hom(A₁,B₁) → Hom(A₂, B₂),其定義為(詳見 hom-functor on ncatlab):

 Hom : (A₂ → A₁ × B₁ → B₂) → Hom(A₁,B₁) → Hom(A₂, B₂)
 Hom (f,g) h = g ∘ h ∘ f

(此處的型別寫法並不很嚴謹,但希望能幫助理解。)

給定函子 FG, 當我們說 h : F → GFG 之間的一個自然變換 (natural transformation), 意思是:h 可看成一系列的態射,對每個物件 A 都有一個態射 h : F A → G A, 並且對任何 f : A → B, 以下式子都成立

 h ∘ F f = G f ∘ h

其中左右兩邊的 h 的型別分別為 F B → G BF A → G A.

伴隨函子的定義中要求 ϕθAB 是自然變換。但由於 Hom 函子比較複雜,這裡的自然變換定義是:對任何 f : A₂ → A₁g : B₁ → B₂,

  ϕ ∘ Hom (L f, g) = Hom (f, R g) ∘ ϕ  
  θ ∘ Hom (f, R g) = Hom (L f, g) ∘ θ

如果我們把 Hom 的定義拆開,在 ϕ 的式子左右兩邊餵一個參數 h : L A₁ → B₁, 在 θ 的式子左右兩邊餵一個參數 k : A₁ → R B₁, 我們分別得到

  ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f  
  θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f

單子規則

有了這些準備,我們終於可以證明單子規則了。

3. η ∘ f = M f ∘ η:

    R (L f) ∘ ϕ id
  =  { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := L f, id, id] }
    ϕ (L f ∘ id ∘ L id)
  = ϕ (L f)
  = ϕ (id ∘ id ∘ L f)
  =  { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h := id, id]}
    ϕ id ∘ f

4. M f ∘ μ = μ ∘ M (M f)

   R (θ id) ∘ (R (L (R (L f)))
 = R (θ id ∘ L (R (L f)))
 =  { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (L f)] }
   R (θ (R id ∘ id, R (L f)))
 = R (θ (R (L f)))
    { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := L f, id, id] } 
 = R (L f ∘ θ id ∘ id)
 = R (L f) ∘ R (θ id)

5.1 μ ∘ η = id

    R (θ id) ∘ ϕ id
  =   { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := θ id, id, id] }
    ϕ (θ id ∘ id ∘ id)
  = ϕ (θ id)
  =   { ϕ ∘ θ = id }
    id


5.2 μ ∘ M η = id

     R (θ id) ∘ R (L (ϕ id))
  = R (θ id ∘ L (ϕ id))
  =  { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, ϕ id] }
    R (θ (R id ∘ id ∘ ϕ id))
  = R (θ (ϕ id))
  =  { θ ∘ ϕ = id }
    R id
  = id .

6. μ ∘ μ = μ ∘ M μ

   R (θ id) ∘ R (L (R (θ id)))
 = R (θ id ∘ L (R (θ id)))
 =  { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (θ id)] }
   R (θ (R id ∘ id ∘ R (θ id)))
 = R (θ (R (θ id)))
 =  { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := θ id, id, id]}
   R (θ id ∘ θ id)
 = R (θ id) ∘ R (θ id) 

上述幾個證明使用到的只有函子規則、ϕθ 為反函數、以及 ϕθ 的自然轉換性質。傳統上,這類證明也許會使用畫圖的方式進行。但對我來說,把自然轉換性質寫成等式子,似乎已足夠讓我在語法層次上搬移符號、湊出我要的證明。

參考資料

Leave a Comment

發佈留言必須填寫的電子郵件地址不會公開。 必填欄位標示為 *