$\gdef\spaces#1{~ #1 ~}$ $\gdef\R{\mathbf{R}}$

首先需要强调的是, 这个公理所涉及到的结构的有效性全都依赖于 意象理论, 而相关基础的严格性保证基本上在 1970 年之前就已经由 William Lawvere 完工. 记 $\mathcal{E}$ 是光滑空间之间的光滑映射构成的范畴, 同时假定 $\mathcal{E}$ 还是笛卡尔闭范畴, 也就是 $\mathcal{E}$ 中的箭头对笛卡尔积封闭.

我们可以从 $\mathcal{E}$ 中选出一条几何直线 $R$, 通过指定 $R$ 上两点 $0$ 和 $1$ 之间的距离作为单位长度来确定其他线段的长度. 发挥一些古希腊精神, 线段的移动可以给出 $R$ 上的加法, 尺规作图所构造的 相似三角形 能给出 $R$ 上的乘法 $\gamma = \alpha\beta$.

因此 $R$ 带有交换环结构, 并且允许经典数学中的对象实数环 $\R$ 成为 $R$ 的模型, 注意这里我们只能考虑 $\R$ 作为环的部分, 因为 $R$ 中存在着幂零元.

Kock–Lawvere 公理说的是, 对任意映射 $f: D \to R$, 存在唯一的 $a,b \in R$, 使得

$$ f(\epsilon) \spaces= a + b \epsilon, \quad \forall \epsilon \in D $$

将这里的 $a$ 换成 $f(0)$, 并完全使用量词叙述, 则是

$$ \forall ~ f \in R^D, ~ \exists! ~ b ~ \text{s.t.} ~ \forall ~ d \in D \quad (f(d) = f(0) + b d) $$

如果说这个公理的形式还不足以暗示它的目的, 那么下面这个推论就完全能做到了.

Axiom is incompatible with the law of excluded middle. Either the one or the other has to leave the scene. In Part I of this book, the law of excluded middle has to leave, being incompatible with the natural synthetic reasoning on smooth geometry to be presented here. In the terms which the logicians use, this means that the logic employed is ‘constructive’ or ‘intuitionistic’. We prefer to think of it just as ‘that reasoning which can be carried out in all sufficiently good cartesian closed categories’.

— Anders Kock, Synthetic Differential Geometry

$\gdef\quads#1{\quad #1 \quad}$ $\gdef\str#1{{\footnotesize #1}}$ $\gdef\C{\mathbf{C}}$ $\gdef\spaces#1{~ #1 ~}$

这样一来, 我们所说的 “将近似修正为严格等于” 就可以精确表示为

$$ \frac{\partial f}{\partial x} \quads= f(x+\varepsilon) ~ \str{中} ~ \varepsilon ~ \str{项的系数} $$

复步微分法 的来源是完全解析的, 但其得到的微分方法却能代数地刻画. 正如我们可以考虑复数的 $z = a+b\sqrt{-1} \in \C$ 矩阵表示

$$ A \spaces= \begin{pmatrix} a & -b \\ b & ~~~a \\ \end{pmatrix} ,\quad \det A \spaces= (a+b\sqrt{-1})(a-b\sqrt{-1}) $$

我们也可以构造 对偶数 $a + b \varepsilon \in R$ 的矩阵表示, 并自动得到微分运算的加法和乘法规则, 这可以被简单地视为 Moler 方法的矩阵版本.

$$ A \spaces= \begin{pmatrix} a & a' \\ 0 & a \\ \end{pmatrix} ,\quad \det A \spaces= (a+b\varepsilon)(a-b\varepsilon) $$

$\gdef\Mat{\operatorname{Mat}}$ $\gdef\d{\operatorname{d}}$ $\gdef\Z{\mathbf{Z}}$ $\gdef\spaces#1{~ #1 ~}$

设 $u, v \in R^R$, $n \in \Z$. 记 $A(u, u') = (\begin{smallmatrix} u & u' \\ 0 & u \end{smallmatrix})$. 从矩阵运算中立刻得到

1. $A(u, u') + A(v, v') \spaces= A(u+v, u'+v')$
2. $A(u, u') - A(v, v') \spaces= A(u-v, u'-v')$
3. $A(u, u') \cdot A(v, v') \spaces= A(uv, u'v + uv')$
4. $A(u, u') \cdot (A(v, v'))^{-1} \spaces= A(uv^{-1}, (u'v - uv')v^{-2})$
5. $(A(u, u'))^n = A(u^n, nu^{n-1}u')$

对于 $e^{A(u,u')}$, 注意 $A(u, u') = A(u, 0) + A(0, u')$, 这里 $(A(0, u))^2 = 0$. 同样可以计算得到 $e^{A(u,u')} = A(e^u, 0) \cdot A(1, u') = A(e^u, e^u u')$. 而对于 $\log A(u,u')$ 我们直接展开为 $\sum_{k \ge 1}\frac{(-1)^{k+1}}{k} \cdot (A-1)^k$ 即可 验证.

$\gdef\Mat{\operatorname{Mat}}$ $\gdef\spaces#1{~ #1 ~}$ $\gdef\d{\operatorname{d}}$ $\gdef\eqdef{\overset{\scriptscriptstyle\text{def}}{=}}$

与 $\Mat_{2 \times 2}(R^R)$ 上的 运算 不同, 复合运算是只位于 $R^R$ 上的, 或者说 $\Mat_{2 \times 2}(R^R)$ 上并没有周知的复合运算. 为了自然地给出 $A: J^1(R, R) \to \Mat_{2 \times 2}(R^R)$ 上的复合, 这里 $J^1$ 是一阶 射流丛. 记 $\square(x)$ 为 $\square_x $, $A(u)$ 为 $A(u,u')$, 考虑显式应用的 $A(u)$, 即

$$ A(u)_x \spaces\eqdef \begin{pmatrix} u_x & u'_x \\ 0 & u_x \end{pmatrix} \spaces\in \Mat_{2 \times 2}(R), \quad x \in R $$

对于 $u: Y \to Z$, $v: X \to Y$. $A$ 上的复合 $A(u) \circ A(v)$ 可定义为 $A(u)_{v_x}$, $(v_x, v'_x) \in A(v)_x$. 我们来验证 $A(u) \circ A(v) = A(u \circ v)$.

$$ \begin{aligned} A(u)_{v_x} &\spaces= \Big(u \cdot \frac{\partial A}{\partial u} + \frac{\d u}{\d x} \cdot \frac{\partial A}{\partial u'}\Big)\Big|_{v_x} \\ &\spaces= u(v_x) \cdot \frac{\partial A}{\partial u} + \frac{\d u(v_x)}{\d v_x} \frac{\d v_x}{\d x} \cdot \frac{\partial A}{\partial u'} \\ &\spaces= A(u(v(x)), u'(v(x))v'(x)) \\ \end{aligned} $$