<译>米田嵌入

上一篇：米田引理

原文地址：https://bartoszmilewski.com/2...

咱们以前已经看到，固定范畴C的一个对象，映射C(a, -)是一个从C到Set的（协变）函子。

x -> C(a, x)

(上域是Set是由于hom集C(a, x)是个集合。)咱们把这个映射叫hom函子——咱们以前也已经定义了它在态射上的行为。

如今让咱们变化这个映射中的a。咱们获得了一个新的映射：给任意的a分配一个hom函子C(a, -)。

a -> C(a, -)

这是个从范畴C的对象到函子的映射，而函子是函子范畴的对象（参见天然变换有关函子范畴的部分）。让咱们用记号[C, Set]表示从C到Set的函子范畴。你也可能会回忆起hom函子就是那些本来的可表函子。

咱们每有一个两范畴的对象之间的映射的时候，就会很天然地问它是不是个函子。换句话说咱们是否能够把一个范畴的态射提高到另外一个范畴。C的态射就只是一个C(a, b)的元素，但函子范畴[C, Set]的态射是天然变换。因此咱们想要找一个从态射到天然变换之间的映射。

让咱们看看可否根据一个态射f :: a->b找到一个天然变换。首先，咱们得看看a和b被映为了什么。它们被映为了两个函子：C(a, -)和C(b, -)。咱们须要这两个函子间的一个天然变换。

接下来就是技巧了：咱们使用米田引理：

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

把通常的F带成hom函子C(b, -)，咱们就获得了：

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

这刚好就是咱们要找的那两个函子间的天然变换，不过有点扭曲：咱们获得了一个天然变换和态射间的映射——这个态射是C(b, a)的一个元素——这家伙的方向“错”了。但这没有什么问题；这只是意味着咱们处理的这个函子是逆变的。

实际上，咱们比所希求的获得了更多。这个从C到[C, Set]的映射可不仅是个逆变函子——它是个彻底忠实函子。彻底性和忠实性是描述函子映射hom集时的性质。

忠实函子是说它在hom集上表现为单射，也就是它把不一样的态射映为不一样的态射。换句话说，它不会合并它们。

彻底函子是说它在hom集上表现为满射，也就是它把一个hom集满映为另外一个，彻底覆盖后者。

数学中的满射在英文中有两种表达：一种是 surjective（满射），另外一种是maps A onto B。也就是 onto在数学中有特殊的含义。这一句话就是做者把两种说法都说了一遍，以解释地更清楚。译者注。

彻底忠实函子是说F在hom集上表现为双射——一个两集合元素间的一一映射。对于源范畴C的每一对对象a和b，都有一个C(a, b)和D(F a, F b)间的双射，其中D是F的靶范畴（咱们这里就是函子范畴[C, Set]）。注意这并非说F就是个对象间的双射。可能会有些D中的对象并不在F的像里，从而咱们不能对这些对象的hom集说任何事情。

嵌入

咱们刚刚所说的这个把C的对象映为了[C, Set]的函子的（逆变）函子：

a -> C(a, -)

就定义了米田嵌入。它把一个范畴C(严格地说，是范畴C^op，由于它是逆变的)嵌入到了函子范畴[C, Set]。这不只仅是把C的对象映为了函子，并且它忠实地维持了它们之间的全部联系。

由于数学家们对函子范畴了解的不少，尤为是那些上域为Set的函子，因此这是个很是有用的结果。咱们能够经过把任意范畴C嵌入它的函子范畴而获得不少关于它的洞见。

固然米田嵌入也有一个对偶版本，它有时叫作逆米田嵌入。注意咱们能够从固定每一个hom集的靶对象（而不是源对象）开始，也就是C(-, a)。这给了咱们一个逆变的hom函子。从C到Set的逆变函子就是咱们熟悉的预层（例如参见极限与余极限）。逆米田嵌入定义了范畴C到预层范畴的嵌入。它在态射上的行为由下式给出：

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

一样地，数学家们对预层范畴也了解不少，因此能把任意范畴嵌入其中实在是个好事。

在Haskell中的应用

Haskell中，米田嵌入被表示成reader函子间的天然变换和（反向）函数的同构：

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

（记住，reader函子等价于((->) a)。）

等价的左边是个多态函数，给定一个a到x的函数和一个b类型的值，就能获得一个类型x的值（我没有用柯里化——也就是去掉了函数b -> x上的那个括号）。要对全部的x都能作这件事，惟一的方式就是咱们的函数知道如何把一个b类型的值转换成一个a类型的值。这必然就隐晦地使用了函数b -> a。

给定这样的一个转换，btoa，就能够定义左边了，让咱们叫它fromY：

fromY :: (a -> x) -> b -> x
fromY :: f b = f (btoa b)

反过来，给定一个函数fromY，咱们能够经过用fromY调用恒等函数重构出这个转换：

fromY id :: b -> a

这构建了类型为fromY的函数到btoa的双射。

审视这个同构的另外一个可能的方式就是它是一个从b到a的函数的CPS编码。参数a->x就是延继（那个处理器）。结果是个从b到x的函数，它须要一个b类型的值，它执行的是延继前复合上被编码的那个函数。

米田嵌入也解释了一些Haskell中数据结构的其余可能的表示方式。尤为是，它根据Control.Lens库提供了一种很是有用的representation of lenses。

这一篇 representation of lenses我没有翻译。米田嵌入是该做者范畴论的第二部分的最后一篇，我尚不知道下一步是先翻译第三部分仍是翻译一些这样的零散文章。在我翻译这一篇以后，我会把翻译以后的连接补过来。译者注。

预序的例子

这是Robert Harper所建议的一个例子。它是米田嵌入在由一个预序定义的范畴上的应用。一个预序就是带上一个顺序关系的集合，这个元素间的顺序关系一般写做<=（小于等于）。预序里之因此有个"预"字是由于咱们只须要这个关系的传递性和自反性而不须要反对称性（因此它是可能成环的）。

一个带有预序关系的集合导出了一个范畴。集合中的元素就是对象，若是对象a和b无法比较或者a <= b是错的，那a到b的态射就没有，或者a <= b，那这个态射就存在，它由a指向b。一个对象到另外一个的态射永远不会多于一个。因该范畴上的hom集要么就是空集，要么就是单例集。这样的范畴称为薄的。

你很容易就能够看出这的确构造了一个范畴：箭头是可复合的，由于若是a <= b而且b <= c那么a <= c；并且这个复合是结合的。咱们还有恒等箭头，由于每一个元素（小于或）等于本身（这个关系的自反性）。

如今咱们能够把逆米田嵌入用到预序范畴上了。特别地，咱们感兴趣的是它在态射上的行为：

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

右边的hom集是非空的，当且仅当a <= b——这时它是个单例集。所以，若是a <= b，就存在一个左边的天然变换。不然就没有这样的天然变换。

那么预序的hom函子间的天然变换到底是什么？它应该是一个从集合C(-, a)到C(-, b)的函数族。在预序里，这些集合中的每个要么是空的要么是单例集。让咱们看看咱们如今所处理的函数都是些什么家伙。

这里的表达略微混乱，不过不影响理解。“这些集合中的每个要么是空的要么是单例集”应指像 C(x, a)和 C(x, b)这样的家伙，而不是 C(-, a)和 C(-, b)。译者注。

从空集到自身有一个函数（也就是空集上的恒等函数），从空集到单例集有个absurd函数(它什么也不作，由于这须要定义一个空集中的元素，但空集里什么也没有)，从单例集到本身也有个函数(单例集的恒等函数)。惟一不被容许的组合方式是把一个单例集映为空集（这个函数把那单个的元素究竟映为了什么呢？）。

因此咱们的天然变换永远不能把单例集和空集连起来。换句话说，若是x <= a(C(x, a)是个单例hom集)那么C(x, b)就不能为空。一个非空的C(x, b)意味着x小于等于b。因此这个问题里天然变换的存在性就须要对于每一个x来讲，若是x <= a那么x <= b。

for all x, x ≤ a ⇒ x ≤ b

另外一边，反米田嵌入告诉咱们天然变换的存在性等价于C(a, b)是非空的，或者说a <= b。把这二者放到一块儿，就获得了:

a ≤ b if and only if for all x, x ≤ a ⇒ x ≤ b

咱们能够直接获得这个结果。直观上说，若是a <= b那么全部比a小的元素都要比b小。反过来，把右边的x替换成a，就获得了a <= b。但你必须认可经过米田嵌入获得这个结果远让人更为兴奋。

天然性

米田引理构造了一个天然变换的集合和一个Set中对象的同构。天然变换是函子范畴[C, Set]的态射。两个函子间天然变换的集合是这个范畴的一个hom集。米田引理是下面这个同构：

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

这个同构能够证实对于F和a都是天然的。换句话说，它在积范畴[C, Set] × C的序对(F, a)上是天然的。注意如今咱们把F当作函子范畴的一个对象。

让咱们考虑下这意味着什么。天然同构是两个函子间的可逆的天然变换。确实，咱们的同构的右边是个函子。这是个从[C, Set] × C到Set的一个函子。它在序对(F, a)上做用的结果是个集合——就是给函子F带入对象a的执行结果。这样的函子叫执行函子。

左边也是个把(F, a)变到天然变换集合[C, Set](C(a, -), F)的一个函子。

为了证实它们是真正的函子，咱们还应该定义它们在态射上的行为。但序对(F, a)和(G, b)之间的态射是什么？这是一对态射,(Φ，f)；第一个是函子间的态射——一个天然变换——第二个是C上的常规态射。

执行函子取序对(Φ, f)并把它映为一个集合F a到G b间的函数。咱们能够轻易地经过Φ在a上的份量（它把F a映为G a）和被G提高后的态射f，构造出这样一个函数：

(G f) ∘ Φ_a

注意，因为Φ有天然性，因此这等同于:

Φ_b ∘ (F f)

我不会证实整个同构的天然性——在构建了函子以后，证实是很是机械化的。它利用了咱们的同构是创建在函子和天然变换上的这样一件事。这很简单，没可能搞错。

挑战

1. 在Haskell中表达逆米田嵌入
2. 证实咱们创建的fromY和btoa之间的双射是个同构（这两个映射是互逆的）。
3. 用米田嵌入处理幺半群。幺半群的那个单个对象对应的是什么函子？幺半群态射对应的是什么天然变换？
4. 协变的米田嵌入在预序上的应用是什么？（Gershom Bazerman所提出的问题）
5. 米田嵌入能够用来把任意函子范畴[C, D]嵌入到函子范畴[[C, D], Set]。指出它在态射（这里是天然变换）上的行为。

致谢

感谢Gershom Bazerman检查个人数学和逻辑。

下一篇：有关态射的一切