目录
  1. 1. 拉回 Pullbacks
    1. 1.1. 泛性质
    2. 1.2. 性质
    3. 1.3. 在编程中
    4. 1.4. 参考
拉回 Pullbacks

拉回 Pullbacks

在范畴论Category Theory中,一个数学分支,拉回Pullback(也称为纤维积或笛卡尔方块)是由具有公共上域的两个态射 f:XZf:X \to Zg:YZg:Y \to Z 组成的图表的极限。拉回经常写作

P=X×ZY.P=X\times _{Z}Y.

In category theory, a branch of mathematics, a pullback (also called a fiber product, fibre product, fibered product or Cartesian square) is the limit of a diagram consisting of two morphisms f:XZf:X \to Z and $ g:Y \to Z $ with a common codomain. The pullback is often written

P=X×ZY.P=X\times _{Z}Y.

泛性质

态射 ffgg 的拉回由一个对象P和两个态射 p1:PXp1 : P → Xp2:PYp2 : P → Y 组成,使得图表

CategoricalPullBack-03

交换Commute。并且拉回 (P,p1,p2)(P, p1, p2) 对这个图表必须是通用的。这便是说,任何其它这样的三元组 $(Q, q1, q2) $ 一定存在惟一的 u:QPu : Q → P 使得图表

CategoricalPullback-04

交换Commute。和所有泛构造Universal Construction一样,拉回如果存在必然在同构的意义下是惟一的。

性质

  • 如果 X×ZYX ×_{Z}Y 存在,那么 Y×ZXY ×_{Z} X 也存在,且存在态射 X×ZYY×ZXX ×_{Z} Y \cong Y ×_{Z} X
  • 拉回一个单态,得到一个单态。

在编程中

如果我们将态射认为是子类is subclass of的映射,并且有如同

CategoricalPullback-04

的继承关系,那么对于继承自 X YX \space YPP 类型来说,同样继承自X YX \space YQQ 类型同样也是 PP 的子类, 当 PPX YX \space Y的直接组合并且不存在函数重载以及额外数据时,类型 QPQ \to P 的转换是安全的

以上的讨论限于具有Duck Typing的语言, 在类似C++的语言中,由于 子类型化是"标配?"Subtyping is nominal我们无法直接表达这样的关系

参考