Skip to main content

第 29 章：拓扑斯（Topoi）

原文：Bartosz Milewski, Category Theory for Programmers, Scala Edition, Chapter 29. 原书 PDF、.tex 源文件及相关图像采用 CC BY-SA 4.0；本译文按同一许可发布。

我知道我们可能正在离编程越来越远，转而深入硬核数学。但你永远不知道下一场编程大革命会带来什么，也不知道需要什么样的数学才能理解它。现在有一些非常有趣的想法在流动，比如带有连续时间概念的函数式响应式编程、用依赖类型扩展 Haskell 的类型系统，或者在编程中探索同伦类型论。

到目前为止，我一直随意地把类型等同于值的集合。严格说来，这并不正确，因为这种做法没有考虑到这样一个事实：在编程中，我们计算值，而计算是一个需要时间的过程，在极端情况下甚至可能不会终止。发散计算是每一种图灵完备语言的一部分。

还有一些基础性的理由说明，集合论也许并不是计算机科学，甚至数学本身的最佳基础。一个很好的类比是：集合论就像绑定到某种特定架构的汇编语言。如果你希望自己的数学能够运行在不同架构上，就必须使用更一般的工具。

一种可能性是用空间替代集合。空间带有更多结构，并且可以不依赖集合来定义。通常与空间相关联的一件事是拓扑，而拓扑对于定义连续性之类的概念是必要的。传统拓扑的处理方式，正如你可能猜到的，是通过集合论。特别是，子集这个概念在拓扑中居于核心地位。毫不意外，范畴论学者把这个想法推广到了 Set 之外的范畴。那种恰好具有适当性质、可以充当集合论替代品的范畴，称为拓扑斯（topos，复数为 topoi）；它提供的东西之一，就是广义的子集概念。

29.1 子对象分类器（Subobject Classifier）​

我们先尝试用函数而不是元素来表达子集这个想法。任意从某个集合 a 到 b 的函数 f，都会定义 b 的一个子集，也就是 a 在 f 下的像。但有许多函数会定义同一个子集。我们需要说得更具体一些。首先，可以关注那些单射函数，也就是不会把多个元素挤压成一个元素的函数。单射函数把一个集合“注入”另一个集合。对于有限集合，你可以把单射函数想象成一组平行箭头，它们把一个集合的元素连接到另一个集合的元素。当然，第一个集合不能大于第二个集合，否则箭头必然会汇合。这里仍然留下一点歧义：可能还存在另一个集合 a'，以及另一个从它到 b 的单射函数 f'，它选出了同一个子集。但你很容易说服自己，这样的集合必须与 a 同构。我们可以利用这一事实，把子集定义为一族单射函数；这些单射函数通过其定义域之间的同构相互关联。更准确地说，设有两个单射函数：

f  :: a  -> b
f' :: a' -> b

如果存在一个同构：

h :: a -> a'

使得：

f = f' . h

那么它们就是等价的。这样一族等价的注入定义了 b 的一个子集。

等价单射定义同一个子集

如果把单射函数替换成单态射，这个定义就可以提升到任意范畴。提醒一下，从 a 到 b 的单态射 m 由它的泛性质定义。对于任意对象 c 以及任意一对态射：

g  :: c -> a
g' :: c -> a

只要满足：

m . g = m . g'

就必须有 g = g'。

单态射的泛性质

在集合上，如果考虑一个函数 m 不是单态射意味着什么，这个定义就更容易理解。它会把 a 中两个不同元素映射到 b 中的同一个元素。于是我们可以找到两个函数 g 和 g'，它们只在那两个元素上不同。随后与 m 后组合就会掩盖这种差异。

后组合掩盖两个映射的差异

还有另一种定义子集的方式：使用一个称为特征函数的单个函数。它是一个从集合 b 到二元素集合 Omega 的函数 chi。这个集合的一个元素被指定为“真”，另一个被指定为“假”。该函数把“真”赋给 b 中那些属于该子集的元素，把“假”赋给不属于该子集的元素。

还剩下一个问题：指定 Omega 中某个元素为“真”是什么意思。我们可以使用标准技巧：使用一个从单元素集合到 Omega 的函数。我们把这个函数称为 true：

true :: 1 -> Omega

从终对象选出 true

这些定义可以用某种方式组合起来，使它们不仅定义什么是子对象，还定义特殊对象 Omega，而且完全不谈元素。这个想法是：我们希望态射 true 表示一个“泛”的子对象。在 Set 中，它从二元素集合 Omega 中选出一个单元素子集。这已经是尽可能泛的情形了。它显然是一个真子集，因为 Omega 还有另一个不属于这个子集的元素。

在更一般的语境中，我们把 true 定义为从终对象到分类对象 Omega 的单态射。但我们还必须定义这个分类对象。我们需要一个把这个对象与特征函数联系起来的泛性质。事实证明，在 Set 中，沿特征函数 chi 对 true 做拉回，会同时定义子集 a，以及把它嵌入 b 的单射函数。下面是这个拉回图：

由特征函数得到子对象的拉回图

我们来分析这个图。拉回方程是：

true . unit = chi . f

函数 true . unit 把 a 的每个元素都映射到“真”。因此，f 必须把 a 的所有元素映射到 b 中那些被 chi 映射为“真”的元素。这些元素按定义正是特征函数 chi 指定的子集中的元素。所以 f 的像确实就是讨论中的子集。拉回的泛性保证了 f 是单射。

这个拉回图可以用来在 Set 之外的范畴中定义分类对象。这样的范畴必须有一个终对象，这让我们能够定义单态射 true。它还必须有拉回；实际要求是它必须拥有所有有限极限（拉回是有限极限的一个例子）。在这些假设下，我们用下面这个性质定义分类对象 Omega：对于每一个单态射 f，都存在唯一的态射 chi，使它补全这个拉回图。

我们来分析最后一句话。构造拉回时，给定的是三个对象 Omega、b 和 1，以及两个态射 true 和 chi。拉回存在意味着我们可以找到最好的这样一个对象 a，它配备两个态射 f 和 unit（后者由终对象定义唯一确定），并且使图交换。

这里我们解的是另一组方程。我们要求解 Omega 和 true，同时让 a 和 b 变化。对于给定的 a 和 b，可能存在也可能不存在一个单态射 f :: a -> b。但如果存在，我们希望它是某个 chi 的拉回。不仅如此，我们还希望这个 chi 由 f 唯一确定。

我们不能说单态射 f 和特征函数 chi 之间存在一一对应，因为拉回只在同构意义下唯一。但请记住我们先前对子集的定义：子集是一族等价的注入。我们可以把它推广为：b 的一个子对象，是一族到 b 的等价单态射。这族单态射与我们图中一族等价的拉回一一对应。

因此，我们可以把 b 的子对象集合 Sub(b) 定义为一族单态射，并看到它同构于从 b 到 Omega 的态射集合：

Sub(b) ~= C(b, Omega)

这恰好是两个函子之间的自然同构。换句话说，Sub(-) 是一个可表示的（反变）函子，它的表示对象就是 Omega。

29.2 拓扑斯（Topos）​

拓扑斯是满足下面条件的范畴：

  1. 它是笛卡尔闭的：拥有所有积、终对象以及指数对象（指数对象定义为积的右伴随）。
  2. 对所有有限图式都有极限。
  3. 拥有一个子对象分类器 Omega。

这组性质使拓扑斯在大多数应用中都非常适合替代 Set。它还拥有一些由定义推出的额外性质。例如，拓扑斯拥有所有有限余极限，包括初对象。

把子对象分类器定义为两个终对象副本的余积（和）很有诱惑力，因为在 Set 中它正是如此，但我们希望保持更一般。满足这一点的拓扑斯称为布尔拓扑斯。

29.3 拓扑斯与逻辑（Topoi and Logic）​

在集合论中，特征函数可以解释为定义集合元素的某个性质，也就是一个谓词：它对某些元素为真，对另一些元素为假。谓词 isEven 会从自然数集合中选出偶数子集。在拓扑斯中，我们可以把谓词的概念推广为从对象 a 到 Omega 的态射。这就是为什么 Omega 有时被称为真值对象。

谓词是逻辑的构造块。拓扑斯包含研究逻辑所需的所有装置。它有对应于逻辑合取（逻辑与）的积，有用于析取（逻辑或）的余积，还有用于蕴含的指数对象。逻辑的所有标准公理在拓扑斯中都成立，除了排中律（或者等价地说，双重否定消去）。因此，拓扑斯的逻辑对应于构造性逻辑或直觉主义逻辑。

直觉主义逻辑一直在稳步获得地位，并从计算机科学中获得了意想不到的支持。经典的排中概念基于一种信念：存在绝对真理。任何命题要么为真，要么为假；或者用古罗马人的说法，tertium non datur（不存在第三种选择）。但我们能够知道某件事为真或为假的唯一方式，是我们能够证明或证伪它。证明是一个过程，一次计算；而我们知道，计算需要时间和资源。在某些情况下，计算也许永远不会终止。如果我们无法在有限时间内证明一个命题，那么声称它为真并没有意义。拓扑斯凭借其更细腻的真值对象，为建模有趣的逻辑提供了更一般的框架。

29.4 挑战（Challenges）​

  1. 证明：沿特征函数对 true 做拉回得到的函数 f 必须是单射。