« Home

Theorem. Lawvere's fixed point [math-0006]

DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES

在一個 cartesian closed category 中，如果 A→ϕBAA \xrightarrow{\phi} B^A 是 point-surjective，則所有 B→fBB \xrightarrow{f} B 都存在不動點 1→sB1 \xrightarrow{s} B （滿足 f∘s=sf \circ s = s ）。

Proof

首先畫出交換圖

figure tex808

其中 δ\delta 的定義是 c↦⟨c,c⟩c \mapsto \langle c, c \rangle ，所以對 1→pA1 \xrightarrow{p} A 來說 δ∘p=⟨p,p⟩\delta \circ p = \langle p, p \rangle 。沿著這個定義，我們知道 (ϕ×1A)∘δ∘p=⟨ϕ∘p,p⟩(\phi \times 1_A) \circ \delta \circ p = \langle\phi\circ p, p\rangle 。根據 point-surjective 我們知道 ϕ∘p\phi \circ p 對每個 pp 來說都是唯一確定的。現在把往下方 BB 的 evev 也畫出，即可得出等式：

f∘ev∘⟨ϕ∘p,p⟩=ev∘⟨ϕ∘p,p⟩f \circ ev \circ \langle\phi\circ p, p\rangle = ev \circ \langle\phi\circ p, p\rangle

換句話說 B→fBB \xrightarrow{f} B 的不動點即是

ev∘⟨ϕ∘p,p⟩ev \circ \langle\phi\circ p, p\rangle