「一對伴隨函子 (adjoint functor) 可以生出單子 (monad)」對一些人來說是「民眾知識」等級的東西 — 好像大家都知道，問出處則說不上來。因為最近的一些研究，我得把相關知識整理一下，順便註記於此。
伴隨函子
給定範疇 C 與 D，與兩個函子(functor) L : C → D 與 R : D → C. 如果給任何 C 之中的物件(object) A 與 D 之中的物件 B，以下的自然同構均成立：
Hom (L A, B) ≅ Hom (A, R B)
我們便說 L 與 R 是一對伴隨函子 (adjoint functor) ，記為 L ⊣ R。其中 L 與 R 分別稱為左伴隨 (left adjoint) 與右伴隨 (right adjoint)。
我們等下會解釋 Hom (A, B) 與自然同構等等概念。目前可暫時理解成：Hom (A, B) 是由 A 到B 的所有態射 (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，以偏序為態射），伴隨函子的意思便是 L 與 R 形成一組 Galois connection.
「同構」意指存在一組函數：ϕ : Hom (L A, B) → Hom (A, R B) 與 θ : Hom (A , R B) → Hom (L A, B), 滿足 ϕ ∘ θ = id 與 θ ∘ ϕ = id，如同前述的 curry 與 uncurry。「自然同構」要求 ϕ 與 θ 對於 A 和 B 必須是自然變換 (natural transformation). 它們的自然轉換性質複雜但重要，我們後面會解釋並用到。
單子與餘單子
如果 L : C → D 與 R : 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 三個運算子。在數學圈子的習慣中，return 與 join 分別寫做 η 與 μ. 相對地，餘單子 N 也有三個運算元：ε : N B -> B, map : (A → B) → N A → N B, 與 δ : N B → N (N B).
如前所述，伴隨函子 L 與 R 可衍生出單子 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, η, μ) 的規則有六條：
M id = idM f ∘ M g = M (f ∘ g)η ∘ f = M f ∘ ηM f ∘ μ = μ ∘ M (M f)μ ∘ η = id = μ ∘ M ημ ∘ μ = μ ∘ M μ
第 1, 2 條要求 M 是一個函子。由於 L 與 R 均為函子，這兩條也立刻成立。第 3, 4 條要求 η 與 μ 是自然變換，第 5, 6 條則和單子的計算比較相關。他們是否真的成立呢？
態射集合與態射函子
為了證明剩下的四條單子性質，我們看看有哪些關於 ϕ 與 θ 的性質可用。而為此，我們回頭看看之前提及，但迅速帶過的態射集合、自然同構等概念。
給定範疇 C 中的兩個物件 A 與 B, 他們之間所有的態射記為 Hom(A,B). （一般說來 Hom(A,B) 不見得是集合。如果它是集合，C 被稱作一個局部小範疇 (locally small category).）(詳見 hom-set on ncatlab)
給定範疇 C，Hom 也是一個 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
（此處的型別寫法並不很嚴謹，但希望能幫助理解。）
給定函子 F 與 G, 當我們說 h : F → G 是 F 與 G 之間的一個自然變換 (natural transformation), 意思是：h 可看成一系列的態射，對每個物件 A 都有一個態射 h : F A → G A, 並且對任何 f : A → B, 以下式子都成立
h ∘ F f = G f ∘ h
其中左右兩邊的 h 的型別分別為 F B → G B 與 F A → G A.
伴隨函子的定義中要求 ϕ 與 θ 對 A 與 B 是自然變換。但由於 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)
上述幾個證明使用到的只有函子規則、ϕ 與 θ 為反函數、以及 ϕ 與 θ 的自然轉換性質。傳統上，這類證明也許會使用畫圖的方式進行。但對我來說，把自然轉換性質寫成等式子，似乎已足夠讓我在語法層次上搬移符號、湊出我要的證明。
參考資料
- adjoint functor on ncatlab.
- Anton Hilado, Adjoint Functors and Monads, June 20, 2017.
- Thorsten Wißmann, Adjunctions and monads. Seminar “Categories in Programming”, June 3, 2015.
- Steve Awodey, Monads and algebras. Course Notes of Category Theory, LMU Munich, Sommer Semester 2011.