3,094
个编辑
更改
跳到导航
跳到搜索
第449行：
第449行： − + − + − + − + − +
→Lawvere不动点定理
====Lawvere不动点定理====
====Lawvere不动点定理====
[[Lawvere不动点定理]]（也称为[[Lawvere对角线定理]]，1969年提出）是范畴论中统一刻画对角线自指与不动点现象的基础定理。它表明，只要一个笛卡尔闭范畴中存在对函数族的通用编码机制，那么输出对象上的所有自变换都必然存在不动点。
[[Lawvere不动点定理]]（也称为[[Lawvere对角线定理]]，1969年提出）是[[范畴论]]中统一刻画[[对角线自指]]与[[不动点]]现象的基础定理。它表明，只要一个[[笛卡尔闭范畴]]中存在对函数族的通用编码机制，那么输出对象上的所有自变换都必然存在不动点。
===== 定理陈述 =====
===== 定理陈述 =====
设 <math>\mathcal{(\mathcal{C})}</math> 为任意'''笛卡尔闭范畴'''（Cartesian closed category, CCC），<math>A</math> 和 <math>Y</math> 是 <math>\mathcal{C}</math> 中的任意对象。
设 <math>\mathcal{(\mathcal{C})}</math> 为任意[[笛卡尔闭范畴]]（Cartesian closed category, CCC），<math>A</math> 和 <math>Y</math> 是 <math>\mathcal{C}</math> 中的任意对象。
如果存在'''弱点满射'''态射:
如果存在[[弱点满射]][[态射]]:
:<math>g : A \to Y^A</math>
:<math>g : A \to Y^A</math>
（即对每一个态射 <math>f : A \to Y</math>，都存在点 <math>x : 1 \to A</math>，使得 <math>x</math> 与 <math>g</math> 的复合恰好是 <math>f</math> 对应的指数对象点 <math>\ulcorner f \urcorner : 1 \to Y^A</math>），
（即对每一个态射 <math>f : A \to Y</math>，都存在点 <math>x : 1 \to A</math>，使得 <math>x</math> 与 <math>g</math> 的复合恰好是 <math>f</math> 对应的指数对象点 <math>\ulcorner f \urcorner : 1 \to Y^A</math>，这里<math>Y^A</math>为指数对象，包含了所有从<math>A</math>到<math>Y</math>的态射），
则对象 <math>Y</math> 具有'''不动点性质'''：对任意自态射 <math>t : Y \to Y</math>，都存在点 <math>y : 1 \to Y</math>，满足:
则对象 <math>Y</math> 具有'''不动点性质'''：对任意自态射 <math>t : Y \to Y</math>，都存在点 <math>y : 1 \to Y</math>，满足:
:<math>y \cdot t = y</math>
:<math>t(y) = y</math>
其逆否命题等价于：若 <math>Y</math> 上存在没有不动点的自态射，则不存在从 <math>A</math> 到 <math>Y^A</math> 的弱点满射。
其逆否命题等价于：若 <math>Y</math> 上存在没有不动点的自态射，则不存在从 <math>A</math> 到 <math>Y^A</math> 的弱点满射。