更改

====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> 的弱点满射。