<译>米田引理

傷城~ 2022-03-07 04:44 371阅读 0赞

上一篇：[可表函子][Link 1]

原文地址：[https://bartoszmilewski.com/2...][https_bartoszmilewski.com_2...]

范畴论中的大多数构造都是其他具体数学领域的泛化。诸如积、余积、幺半群和指数等等，早都在范畴论以前被了解了。在不同的数学分支中，它们也许有不同的名字。集合论中的笛卡儿积，序数理论的下确界，逻辑中的连词——他们都是范畴积这样一个抽象观点的具体例子。

但作为一个有关范畴的一般陈述，米田引理却完全不同。它少有或没有其他数学分支中的先例。有些人说与它最靠近的类比是群论中的凯莱定理（每个群都同构于某个集合的置换群）。

米田引理的设定是一个任意范畴*C*和一个从*C*到**Set**的函子`F`。我们已经在之前的部分看到过一些指向**Set**的函子是可表的，也就是同构于一个hom函子。米田引理是说所有指向**Set**的函子都能通过自然变换从hom函子获得，而且米田引理精确的列举了所有这样的变换。

在讨论自然变换的时候，我曾说过自然性条件可能非常严格。当你定义一个自然变换在一个对象上的分量的时候，自然性得强到可以把这个分量“搬”到另一个对象的分量上，而这另一个对象和原对象有态射连接。源范畴和靶范畴的箭头越多，你要搬运自然变换的分量的限制就越多。**Set**碰巧就是一个箭头非常多的范畴。

米田引理告诉我们，一个hom函子和任意其他函子`F`间的自然变换被它的单个分量在一个点的取值完全决定！这个自然变换剩下的部分仅仅遵循自然性条件。

所以让我们再来看看米田引理所用到的两个函子间的自然性条件吧。第一个函子是hom函子。它把*C*的任意对象`x`映为态射的集合`C(a, x)`——`a`是*C*中的一个固定对象。我们也已经看到过它把任意`x`到`y`的态射`f`映为`C(a, f)`。

第二个函子是任意指向**Set**的函子`F`。

让我们把这两个函子间的自然变换称作`α`。因为我们是在**Set**中操作，像`α_x`或`α_y`这样的自然变换分量就只是常规的集合间的函数：

α_x :: C(a, x) -> F x
    a_y :: C(a, y) -> F y

![yoneda1][]

而因为这些都是函数，我们就可以看看它们在具体点上的值。但集合`C(a, x)`里的点是什么？这就是关键的观察了：集合`C(a, x)`的每个点也是个从`a`到`x`的态射`h`。

所以`α`的自然性四方图：

α_y ∘ C(a, f) = F f ∘ α_x

逐点作用在`h`上时，就变成了：

α_y (C(a, f) h) = F f (α_x h)

你可以从之前的部分回想起hom函子`C(a, -)`在态射`f`上的行为就被定义为前复合：

C(a, f) h = f ∘ h

这就导出了：

α_y (f ∘ h) = (F f) (α_x h)

这个条件究竟有多强看看让`x`等于`a`的情形就知道了。

![yoneda2][]

这时`h`变成了一个从`a`到`a`的态射。我们知道至少存在一个这样的态射，`h = id_a`。让我们把它带入：

α_y f = (F f) (α_a id_a)

注意发生了什么：左边是`α_y`在`C(a, y)`的任意元素`f`上的作用。并且它由`α_a`在`id_a`的这单单一个值所完全决定。我们可以任意选取这样的值，这样就生成了一个自然变换。因为`α_a`的值落在集合`F a`中，所以`F a`的任意点都定义了某个`α`。

反过来，给定任意从`C(a, -)`到`F`的自然变换`α`，你可以计算出它在`id_a`的值，从而得到一个`F a`的点。

这样我们就证明了米田引理：

> 从 `C(a, -)`到 `F`的自然变换和 `F a`的元素是一一对应的。

换句话说，

Nat(C(a, -), F) ≅ F a

或者说，如果我们用记号`[C, Set]`表示*C*和**Set**间的函子范畴，自然变换的集合就只是这个范畴的一个hom集了，并且我们可以写成：

[C, Set](C(a, -), F) ≅ F a

这个对应实际上是个自然同构，我之后会解释这是怎么回事。

现在让我们试着直观感受下这个结果。最让人惊讶的莫过于整个自然变换从一个凝结点开始结晶了：凝结点就是自然变换作用于`id_a`的值。在自然性条件下，自然变换从该点向外延伸。它覆盖了**Set**中所有*C*的像。所以我们首先考虑下*C*在`C(a, -)`的像。

让我们从`a`自己的像开始。在hom函子`C(a, -)`下，`a`被映为集合`C(a, a)`。另一方面，在函子`F`下，它被映为集合`F a`。自然变换的分量`α_a`是某个从`C(a, a)`到`F a`的函数。让我们仅仅关注`C(a, a)`的一个点，也就是那个对应于态射`id_a`的点。为了强调它只是集合中的一个点，我们把它叫做`p`。分量`α_a`应当把`p`映为`F a`的某个点`q`。我将给你证明任意`q`的选择会导出唯一的自然变换。

![yoneda3][]

第一个断言是`q`的选择会唯一决定函数`α_a`的剩余部分。真的，让我们任选`C(a, a)`的另一个点`p'`，它对应某个从`a`到`a`的态射`g`。接下来就是米田引理的魔法时刻了：`g`可以被看成集合`C(a, a)`的某个点`p'`,同时它还对应着两个集合间的*函数*。确实，在hom函子下，态射`g`被映为函数`C(a, g)`；在`F`下它被映为`F g`。

![yoneda4][]

现在我们考虑`C(a, g)`在我们原始的`p`上的作用，`p`就是对应着`id_a`的那个家伙。这定义成前复合，`g∘id_a`，它就是`g`，也对应着我们的点`p'`。所以态射`g`被映为了一个把`p`映为`p'`的函数，而`p'`就是`g`。我们整整兜了一圈！

现在考虑`F g`在`q`上的作用。这会是某个`q'`，`F a`的一个点。为了补全自然四方图，`p'`必须在`α_a`下被映为`q'`。我们选取了任意的`p'`(也就是任意的`g`)然后得到了它在`α_a`下的像，因此函数`α_a`完全确定了。

第二个断言是对于*C*中的任意和`a`有连接的对象`x`，`α_x`会被唯一决定。原因是类似地，只不过现在我们多了两个集合`C(a, x)`和`F x`，并且从`a`到`x`的态射`g`在hom函子下被映为了：

C(a, g) :: C(a, a) -> C(a, x)

而在`F`下被映为：

F g :: F a -> F x

同样地，`C(a, g)`在我们的`p`上的作用由前复合给出：`g ∘ id_a`，这对应了`C(a, x)`的一个点`p'`。自然性决定了`α_x`作用在`p'`上的值会是：

q' = (F g) q

因为`p'`是任取的，所以因此整个`α_x`被确定了。

![yoneda5][]

如果*C*中有和`a`没有连接的对象呢？它们在`C(a, -)`下会统统被映为一个集合——空集。回忆一下，空集是集合范畴的初始对象。这意味着从它到任意其他集合只有一个函数。我们曾把它叫做`absurd`。所以同样地，我们仍然没有选择自然变换分量的余地：它只能是`absurd`。

一个理解米田引理的方法是把指向**Set**的函子间的自然变换们就看作一堆函数族，而函数通常是会损失信息的。一个函数可能会坍缩信息，并且它可能只覆盖上域的一部分。那些仅有的不会损失信息的函数就是那些可逆函数——同构。因此呢，最好的保持结构的指向**Set**的函子就是那些可表的。它们或者是hom函子，或者和hom函子自然同构。任何其他从hom函子得到函子`F`的过程都损失了信息。这样的变换可能不止损失了信息，它也可能只覆盖了函子`F`在**Set**上像的一小部分。

# Hasekll中的米田引理 #

我们已经遇到过Haskell中伪装成reader函子的hom函子了：

type Reader a x = a -> x

reader通过前复合映射态射（这里就是函数）：

instance Functor (Reader a) where
        map f h = f . h

米田引理告诉我们reader函子可以被自然地映为其他函子。

一个自然变换就是一个多态函数。所以给定一个函子`F`，我们就有一个由reader函子到它的映射：

alpha :: forall x . (a -> x) -> F x

通常来说，`forall`是可以省略的，但我想把它明确地写出来以强调自然变换的参数化多态性质。

米田引理告诉我们这些自然变换和`F a`的元素们一一对应：

forall x . (a -> x) -> F x ≅ F a

这个等价的右边一般被看作一个数据结构。还记得把函子看作容器的推广的解释吗？`F a`是一个`a`的容器。但左边是个以一个函数作为参数的多态函数。米田引理说这两种表达等价——它们包含了同样地信息。

另一个说法是：给我一个这种类型的多态函数：

alpha :: forall x . (a -> x) -> F x

我就能得到一个`a`的容器。技巧就是我们之前在米田引理的证明中用到过的：我们用`id`调用这个函数就得到了`F a`的一个元素：

alpha id :: F a

反过来也对。给定一个`F a`的值：

fa :: F a

就可以定义一个恰当类型的多态函数：

alpha h = fmap h fa

你可以轻易地在这两种表达间来回切换。

多种表达的好处是其中一种可能比另一种易于复合，或者某些应用中一种可能比另一种更有效率。

这个原理地最简单示例就是经常用在编译器构造中地编码转换：延继传递风格或CPS。这是米田引理在恒等函子上最简单的应用。把`F`换成恒等函子就得到了：

forall x . (a -> r) -> r ≅ a

> 关于延继传递风格（Continuation-passing style，CPS），网上的叫法不一，但大多把continuation译为“延续”，我觉得不妥。因为在CPS中，把需要传递的类型为 `(a -> r)`的函数就叫the continuation。称呼一个函数为延续毕竟有些口语，不符合数学的习惯，于是我就自作主张的译为“延继”了。译者注。

这个公式的解释是任意类型`a`可以被代替成一个以一个`a`的“处理器”为参数的函数。一个处理器就是一个接受`a`为参数并执行后续计算的函数——延继。（类型`r`通常封装成某种类型的状态码）

这种编程风格在用户界面编程、异步系统和并行编程中都非常普遍。CPS的缺点是它设计了控制的反向。开发端和用户（处理器端）的代码是分离的，这就不易于复合。谁要是做过些一般的web编程，就会了解交互式状态处理程序的面条代码的噩梦了。就像我们之后会看到的，如果函子和单子使用得当，就能存储一些CPS的可复合性质了。

# 逆米田引理 #

就像以往一样，我们通过将箭头反向得到了额外的构造。米田引理可以应用到反范畴*C\_op*从而给出逆变函子间的映射。

等价的说，我们通过固定hom函子的靶对象而不是源对象得到了逆米田引理。我们得到从*C*到**Set**的逆变hom函子：`C(-, a)`。米田引理的这个逆变版本构建了这个函子到其他任意逆变函子`F`间的自然变换与集合`F a`的元素之间的一一对应：

Nat(C(-, a), F) ≅ F a

这儿是逆米田引理Haskell版本：

forall x . (x -> a) -> F x ≅ F a

注意，有些文献中把这个逆变版本就叫米田引理。

# 挑战 #

1.  证明这两个在Haskell中组成米田同构的函子`phi`和`psi`互逆。
    
        phi :: (forall x . (a -> x) -> F x) -> F a
        phi alpha = alpha id
    
        psi :: F a -> (forall x . (a -> x) -> F x)
        psi fa h = fmap h fa
2.  所谓离散范畴就是指有一些对象，但除了恒等态射外没有别的态射的范畴。米田引理是如何处理从这个范畴出发的函子的？
3.  unit的列表`[()]`除了它的长度不包含任何其他信息。所以，作为一个数据类型，它可以视为整数的一个编码方式。空列表代表0，单例列表`[()]`(这是一个值，并不是类型)表示1，等等。请使用米田引理构造出这个列表函子的另一种表示。

# 参考文献 #

1.  [Catsters][] video

# 致谢 #

感谢Gershom Bazerman检查我的数学和逻辑，以及André van Meulebrouck在整个系列中的编辑上的帮助。

下一篇：[米田嵌入][Link 2]

[Link 1]: https://segmentfault.com/a/1190000017971731
[https_bartoszmilewski.com_2...]: https://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/
[yoneda1]: /images/20220307/f2596b0ec83d4194a74ee7583c4fb25a.png
[yoneda2]: /images/20220307/336f49554942446986ab47f4ab4b8618.png
[yoneda3]: /images/20220307/e2df929ca7314a6a8c67da12e1fa876a.png
[yoneda4]: /images/20220307/10c7f94df51d49e6a1198e7a2f4387da.png
[yoneda5]: /images/20220307/168df497e3464a48a22ec027929bf452.png
[Catsters]: https://www.youtube.com/watch?v=TLMxHB19khE
[Link 2]: https://segmentfault.com/a/1190000018175669