更改

'''Lawvere定理（范畴论版本）'''：设 <math>\mathcal{C}</math> 为任意[[笛卡尔闭范畴]]（Cartesian closed category, CCC），<math>A</math> 和 <math>Y</math> 是 <math>\mathcal{C}</math> 中的任意对象。

'''Lawvere定理（范畴论版本）'''：设 <math>\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>f : 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>Y^A</math>为指数对象，包含了所有从<math>A</math>到<math>Y</math>的态射），则对象 <math>Y</math> 具有'''不动点性质'''：对任意自态射 <math>t : Y \to Y</math>，都存在点 <math>z : 1 \to Y</math>，满足:

（即对每一个态射 <math>g : A \to Y</math>，都存在点 <math>x : 1 \to A</math>，使得 <math>x</math> 与 <math>f</math> 的复合恰好是 <math>g</math> 对应的指数对象点 <math>\ulcorner g \urcorner : 1 \to Y^A</math>，这里<math>Y^A</math>为指数对象，包含了所有从<math>A</math>到<math>Y</math>的态射），则对象 <math>Y</math> 具有'''不动点性质'''：对任意自态射 <math>\alpha : Y \to Y</math>，都存在点 <math>t : 1 \to Y</math>，满足:

:<math>t(z) = z</math>

:<math>\alpha(t) = t</math>

其逆否命题等价于：若 <math>Y</math> 上存在没有不动点的自态射，则不存在从 <math>A</math> 到 <math>Y^A</math> 的弱点满射。

其逆否命题等价于：若 <math>Y</math> 上存在没有不动点的自态射，则不存在从 <math>A</math> 到 <math>Y^A</math> 的弱点满射。

#: <math>\mathcal{C}(A \times X, Y) \cong \mathcal{C}(X, Y^A)</math>

#: <math>\mathcal{C}(A \times X, Y) \cong \mathcal{C}(X, Y^A)</math>

#: 即二元态射与“返回函数的一元态射”一一对应。从右向左的逆变换称为'''逆柯里化'''（逆<math>\lambda</math>变换）。

#: 即二元态射与“返回函数的一元态射”一一对应。从右向左的逆变换称为'''逆柯里化'''（逆<math>\lambda</math>变换）。

# '''弱点满射'''：态射 <math>g : A \to Y^A</math> 称为'''弱点满射'''，当且仅当：对任意一元态射 <math>f : A \to Y</math>，都存在点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有

# '''弱点满射'''：态射 <math>f : A \to Y^A</math> 称为'''弱点满射'''，当且仅当：对任意一元态射 <math>g : A \to Y</math>，都存在点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有

#: <math>\langle a, y \rangle \cdot \bar{g} = a \cdot f</math>

#: <math>\langle a, y \rangle \cdot \bar{f} = a \cdot f</math>

#: 其中 <math>\bar{g} : A\times A \to Y</math> 是 <math>g</math> 的逆柯里化。

#: 其中 <math>\bar{f} : A\times A \to Y</math> 是 <math>g</math> 的逆柯里化。

#: 直观含义：所有从 <math>A</math> 到 <math>Y</math> 的一元函数，都可以被 <math>A</math> 中的某个点 <math>y</math> 通过通用二元函数 <math>\bar{g}</math> 表示。

#: 直观含义：所有从 <math>A</math> 到 <math>Y</math> 的一元函数，都可以被 <math>A</math> 中的某个点 <math>y</math> 通过通用二元函数 <math>\bar{f}</math> 表示。

详细证明：

详细证明：

* 步骤1：逆柯里化得到通用二元态射

* 步骤1：逆柯里化得到通用二元态射

*: 根据指数伴随的柯里化同构，态射 <math>g : A \to Y^A</math> 唯一对应一个二元态射 <math>\bar{g} : A \times A \to Y</math>（称为 <math>g</math> 的逆柯里化），满足：

*: 根据指数伴随的柯里化同构，态射 <math>f : A \to Y^A</math> 唯一对应一个二元态射 <math>\bar{f} : A \times A \to Y</math>（称为 <math>f</math> 的逆柯里化），满足：

*: <math>\bar{g} = (A \times g) \cdot \epsilon_A</math>

*: <math>\bar{f} = (A \times f) \cdot \epsilon_A</math>

*: 其中 <math>A \times g</math> 是积函子作用在态射 <math>g</math> 上的结果。

*: 其中 <math>A \times f</math> 是积函子作用在态射 <math>f</math> 上的结果。

*: 直观上，<math>\bar{g}</math> 是范畴内部的“通用解释器”：第一个参数是输入值，第二个参数是函数的编码，输出函数作用在输入上的结果。

*: 直观上，<math>\bar{f}</math> 是范畴内部的“通用解释器”：第一个参数是输入值，第二个参数是函数的编码，输出函数作用在输入上的结果。

* 步骤2：构造对角线复合函数

* 步骤2：构造对角线复合函数

*: 取对角态射 <math>\delta_A : A \to A \times A</math>，将其与 <math>\bar{g}</math>、<math>t</math> 依次复合，得到一元态射 <math>f : A \to Y</math>：

*: 取对角态射 <math>\delta_A : A \to A \times A</math>，将其与 <math>\bar{f}</math>、<math>t</math> 依次复合，得到一元态射 <math>g : A \to Y</math>：

*: <math>f = \delta_A \cdot \bar{g} \cdot t</math>

*: <math>g = \delta_A \cdot \bar{f} \cdot \alpha</math>

*: 对任意点 <math>x : 1 \to A</math>，<math>f</math> 的作用可展开为：

*: 对任意点 <math>x : 1 \to A</math>，<math>g</math> 的作用可展开为：

*: <math>x \cdot f = t\left( \langle x, x \rangle \cdot \bar{g} \right)</math>

*: <math>x \cdot g = \alpha\left( \langle x, x \rangle \cdot \bar{f} \right)</math>

*: 其含义是：先将输入 <math>x</math> 复制一份，同时作为 <math>\bar{g}</math> 的两个参数代入（对角线操作），再将计算结果用 <math>t</math> 做变换。这是整个证明的核心——抽象的对角线自指代入。

*: 其含义是：先将输入 <math>x</math> 复制一份，同时作为 <math>\bar{f}</math> 的两个参数代入（对角线操作），再将计算结果用 <math>\alpha</math> 做变换。这是整个证明的核心——抽象的对角线自指代入。

* 步骤3：应用弱点满射条件

* 步骤3：应用弱点满射条件

*: 根据题设，<math>g</math> 是弱点满射。对上述构造的 <math>f : A \to Y</math>，必然存在某个点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有：

*: 根据题设，<math>f</math> 是弱点满射。对上述构造的 <math>g : A \to Y</math>，必然存在某个点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有：

*: <math>\langle a, y \rangle \cdot \bar{g} = a \cdot f</math>

*: <math>\langle a, y \rangle \cdot \bar{f} = a \cdot g</math>

*: 也就是说，<math>y</math> 就是函数 <math>f</math> 对应的“编码”。

*: 也就是说，<math>y</math> 就是函数 <math>g</math> 对应的“编码”。

* 步骤4：对角线代入导出不动点等式

* 步骤4：对角线代入导出不动点等式

*: 将上式中的任意点 <math>a</math> 替换为编码点 <math>y</math> 本身（即将编码代入自身的参数位，完成自指闭合），可得：

*: 将上式中的任意点 <math>a</math> 替换为编码点 <math>y</math> 本身（即将编码代入自身的参数位，完成自指闭合），可得：

*: <math>\langle y, y \rangle \cdot \bar{g} = y \cdot f</math>

*: <math>\langle y, y \rangle \cdot \bar{f} = y \cdot f</math>

*: 将右侧的 <math>f</math> 按步骤2的定义展开，代入 <math>y \cdot f = t\left( \langle y, y \rangle \cdot \bar{g} \right)</math>，得到：

*: 将右侧的 <math>g</math> 按步骤2的定义展开，代入 <math>y \cdot g = \alpha\left( \langle y, y \rangle \cdot \bar{f} \right)</math>，得到：

*: <math>\langle y, y \rangle \cdot \bar{g} = t\left( \langle y, y \rangle \cdot \bar{g} \right)</math>

*: <math>\langle y, y \rangle \cdot \bar{f} = \alpha\left( \langle y, y \rangle \cdot \bar{f} \right)</math>

*: 令 <math>z = \langle y, y \rangle \cdot \bar{g}</math>，这是 <math>Y</math> 的一个点，则上式可写为：

*: 令 <math>t = \langle y, y \rangle \cdot \bar{f}</math>，这是 <math>Y</math> 的一个点，则上式可写为：

*: <math>z = z \cdot t</math>

*: <math>t = \alpha(t)</math>

* 步骤5：结论

* 步骤5：结论