Ancker-0 Ancker-0 记录一下学习范畴论的时候遇到的第一个稍微有点复杂的证明，顺便学一下怎么画简单的交换图。
固定一个 \(I\) 到 \(C\) 的函子 \(D\) 。一个以 \(c\) 为顶点的 cone，可以看作 \(\Delta_c\) 到 \(D\) 的自然变换，其中 \(\Delta_c\) 表示把所有对象映到 \(c\) 、所有态射映到 \(\op{id}_c\) 的函子。同时， \(\Hom(-, d)\) 和 \(\Nat(\Delta_{(-)}, D)\) 是 \(C\) 到 \(\Set\) 的逆变函子。 如果存在一个 cone \(U \in \Nat(\Delta_d, D)\) ，使得对任意一个 cone \(K \in \Nat(\Delta_c, D)\) 都存在 \(C\) 中唯一的态射 \(h : c \to d\) 使得 \(K = \op{contramap} h\; U\) ，那么就称 \(U\) 是 universal cone， \(U\) 的顶点 \(d\) 是 \(\lim D\) 。可以证明，如果 \(\lim D\) 存在，那么所有 \(\lim D\) 是同构的（换言之， \(\lim D\) 在同构意义下唯一）。
下面我们来证明， \(D\) 存在极限 \(d = \lim D\) ，当且仅当，存在 \(\Hom(-, d)\) 到 \(\Nat(\Delta_{(-)}, D)\) 的自然同构。
如果你理解了这个命题在说什么，那么有一个方向是容易的。设 \(d=\lim D\) ，对应的 universal cone 是 \(U\) 。我们要构造出一个自然同构 \(\eta_c : \Hom(c, d) \to \Nat(\Delta_c, D)\) ，实际上这个映射直接由 \(\eta_c(h) = U \circ h\) 给出，而它是双射的原因就在于 \(U\) 是 universal cone（definition!）。而自然条件（交换四边形）同样是自然的。
另一个方向有一些绕。给定一个自然同构 \(\eta\) ，我们就能说明 \(d=\lim D\) 了吗？答案是肯定的。一切都蕴含在下面这个交换图 \(\eqref{1}\) 中。 首先，任取一个以 \(c\) 为顶点的 cone \(K \in \Nat(\Delta c, D)\) ，我们的目标是证明存在 \(c\) 到 \(d\) 的唯一一个态射 \(h\) ，使得 \(K\) 就是 universal cone 复合上 \(h\) 。注意到 \(\eta_c^{-1}\) 给出了一个 \(h \in \Hom(c, d)\) ，这时可以考虑 \(\eta\) 把 \(h\) 映到的交换四边形（回顾我们在自然变换学到的知识，自然变换把对象映射到态射，把态射映射到交换四边形），也就是下面这个交换图 \(\eqref{1}\) 。注意到图中的对象都是集合，箭头都是函数，于是我们可以考虑集合里的一个元素经过这些函数会变成什么。事实上，如果把右上角的 \(\Hom(d, d)\) 用 \(\id_d\) 替换，我们可以得到如下的交换图。这基本上就是我们要证的结论。我们声称 \(U = \eta_d(\id_d)\) 就是 universal cone，那么由 \(\eqref{2}\) 的交换性， \(K = \op{contramap} h\; U = U \circ h\) ，另一方面，如果有一个 \(h'\) 使得 \(K = U \circ h'\) ，那么下图把 \(h\) 换成 \(h'\) 依然是交换的，但是 \(\eta_c\) 是一个同构，这意味着 \(h=h'\) ，也就是说 \(h\) 是唯一的。这就证明了 \(d = \lim D\) 。
\[ \begin{equation}\tag{1}\label{1} \begin{CD} \Hom(c, d) @<\operatorname{cmap} h<< \Hom(d, d) \\ @V\eta_c V \cong V @V\eta_{d} V \cong V\\ \Nat(\Delta_c, D) @<\operatorname{cmap} h<< \Nat(\Delta_d, D) \end{CD} \end{equation} \]
\( \begin{equation}\tag{2}\label{2} \begin{CD} h @<\operatorname{cmap} h<< \text{id}_d \\ @V\eta_c V \cong V @V\eta_{d} V \cong V\\ K @<\operatorname{cmap} h<< U \end{CD} \end{equation} \)
文中证明的结论来自 Category Theory for Programmers ，作者表示：
I'm not going to go through the proof of this statement. The procedure is pretty straightforward if not tedious.
但是另一方向的证明并不十分显然，除非意识到 \(\eta_d(\id_d)\) 就是 universal cone。
另外，猫论系列的第一篇在 CALand ，第二篇现在还是草稿，也许有时间的话我会把它们迁过来。前几天在讨论班上证明了这个命题，就把第三篇先发出来了。
Yoneda Lemma 有一个非常类似的交换图： \[ \begin{CD} \Hom(a, a) @>\Hom(a, h)>> \Hom(a, c) \\ @V\alpha_aVV @V\alpha_cVV \\ F a @>F h>> F c \\ \end{CD}\] \[\begin{CD} \id_a @>\Hom(a, h)>> h \\ @V\alpha_aVV @V\alpha_cVV \\ \alpha_a(\id_a) @>F h>> \alpha_c(h) \\ \end{CD} \] 所以……也许可以用 Yoneda Lemma 简化前面的证明？ 未完待续……
Yoneda Lemma 在 programming 里有一个很 intuitive 的解释。考虑一个函子 \(F\) ，可以得到一个 fmap :: (a -> b) -> (F a -> F b) 。然后可以改变一下参数顺序，得到一个 F a -> (a -> b) -> F b 。这是在说，给定一个类型是 F a 的对象，就可以获得一个 forall b . (a -> b) -> F b 的映射。我们可以反过来，如果有一个 forall b . (a -> b) -> F b 的映射，那么可以取 a = x ，然后代入 ida 得到那个 F a 的对象。这基本上就是 Yoneda Lemma 在说的事情： F a 和 \(\Nat(\Hom(a, -), F)\) （也就是 forall b . (a -> b) -> F b ）同构。