<div class="article fmt article__content">
<p>上一篇：<a href="https://segmentfault.com/a/1190000017957156">自由幺半群</a></p>
<p>原文地址：<a href="https://bartoszmilewski.com/2015/07/29/representable-functors/">https://bartoszmilewski.com/2...</a></p>
<p>是时候谈谈集合了。数学家们对集合论是又爱又恨。它是数学中的汇编语言——至少它常常是。范畴论在某种程度上尝试跳出集合论，一个众所周知得事实就是不存在所有集合的集合，但所有集合的范畴，<strong>Set</strong>，是存在的。这就很好。另一方面，我们假定一个范畴中任意两个对象之间的态射构成一个集合。我们还叫它hom集。为了公平，还有一种范畴论中态射并不构成集合。取而代之的是它们是另一个范畴中的对象。这些范畴使用的不是hom集而是hom对象，它们被称作<em>富</em>范畴。然而，接下来，我们还将只看那些使用可爱的原始形式的hom集的范畴。</p>
<blockquote>
富范畴的原文为enriched category，我没有找到它对应的中文。译者注。
</blockquote>
<p>集合是你能找到的最接近范畴对象的平凡的家伙了。一个集合有元素，但你不能对这些元素说更多的事。如果你有一个有限集，那么你能数出他们来。你可以用基数大致对无限集的元素计数。比如，自然数集小于实数集，即使它们都是无限多的。但是，可能有些让人惊讶的是，有理数集和自然数集一样大。</p>
<p>除此之外，所有有关集合的信息都能表现在它们之间的函数上——尤其是叫做同构的那些可逆的家伙。同构的集合在任何意义下都是完全一样的。在我引起基础数学家们的愤怒之前，让我解释一下：相等和同构的区别具有非常根本的重要性。实际上它是数学最新的分支，同伦类型论（the Homotopy Type Theory ,HoTT）关心的主要问题之一。我提到HoTT是因为它是灵感来源于计算的一门纯粹的数学理论，而它主要的支持者之一，Vladimir Voevodsky，主要是在研究Coq定理证明辅助器时顿悟的。数学和编程的互动是双向的。</p>
<p>关于集合的重要的一课是，不想元素那样，集合是可以比较的。比如，我们可以说一个给定的自然变换的集合同构于某个态射的集合，因为一个集合就只是一个集合。在这个例子里同构就只是说对于一个集合里的每个自然变换另一个集合里都有唯一的一个态射与之对应，反之亦然。他们可以互相配对。如果苹果和橘子是不同的范畴里的对象，那你不能比较苹果和橘子，但你可以比较苹果的集合和橘子的集合。通常把一个范畴问题转换成一个集合论的问题会给我们一些必要的直观或者甚至让我们证明有价值的定理。</p>
<h1>Hom函子</h1>
<p>每个范畴都天生具有一个到<strong>Set</strong>的典型映射族。这些映射实际上是函子，所以它们维持范畴的结构。让我们构造一个这样的映射。</p>
<p>我们固定<em>C</em>的一个对象<code>a</code>然后选择另一个对象<code>x</code>，hom集<code>C(a, x)</code>是个集合，也就是<strong>Set</strong>的一个对象。当我们保持<code>a</code>固定不变而变化<code>x</code>时，<code>C(a, x)</code>也会在<strong>Set</strong>中变动。因此我们有了个从<code>a</code>到<strong>Set</strong>的映射。</p>
<p><span class="img-wrap"><img alt="hom-set" src="https://beijingoptbbs.oss-cn-beijing.aliyuncs.com/cs/5606289-96e4dd282739cd34b94561c875ae14e9" title="hom-set"></span></p>
<p>如果我们想强调我们正把hom集看作以它的第二个参数作自变量的映射，就使用记号：</p>
<pre class="blockcode"><code class="nohighlight">C(a, -)</code></pre>
<p>其中连接号充当了该参数的占位符。</p>
<p>对象的映射可以容易地拓展到态射的映射。我们取C中两个任意对象<code>x</code>和<code>y</code>的态射<code>f</code>。在我们刚刚定义的映射下，对象<code>x</code>被映为集合<code>C(a, x)</code>而<code>y</code>被映为<code>C(a, y)</code>。如果该映射要成为一个函子，<code>f</code>必须被映为这两个集合之间的一个函数：</p>
<pre class="blockcode"><code class="nohighlight">C(a, x) -> C(a, y)</code></pre>
<p>让我们逐点定义这个函数，逐点就是分别对每个取值分别处理。这里我们应该选取<code>C(a, x)</code>中的一个任意元素——我们叫它<code>h</code>好了。首尾相连的态射是可复合的。<code>h</code>的尾和<code>f</code>的头就是这种匹配的情况，所以它们的复合：</p>
<pre class="blockcode"><code class="nohighlight">f h :: a -> y</code></pre>
<p>是一个<code>a</code>到<code>y</code>的态射。因此它是<code>C(a, y)</code>的一个家伙。</p>
<p><span class="img-wrap"><img alt="hom-functor" src="https://beijingoptbbs.oss-cn-beijing.aliyuncs.com/cs/56 |
|
转播
