nLab Lawvere's fixed point theorem

Redirected from "Lawvere fixed point theorem".
Contents

Contents

Idea

Various diagonal arguments, such as those found in the proofs of the halting theorem, Cantor's theorem, and Gödel‘s incompleteness theorem, are all instances of the Lawvere fixed point theorem (Lawvere 69), which says that for any cartesian closed category, if there is a suitable notion of epimorphism from some object AA to the exponential object/internal hom from AA into some other object BB

AB A A \longrightarrow B^A

then every endomorphism f:BBf \colon B \to B of BB has a fixed point.

Precise statement

Let us say that a map ϕ:XY\phi: X \to Y is point-surjective if for every point q:1Yq: 1 \to Y there exists a point p:1Xp: 1 \to X that lifts qq, i.e., ϕp=q\phi p = q.

Theorem

(Lawvere’s fixed-point theorem) In a cartesian closed category, if there is a point-surjective map ϕ:AB A\phi: A \to B^A, then every morphism f:BBf: B \to B has a fixed point s:1Bs: 1 \to B (so that fs=sf s = s).

Proof

Given f:BBf: B \to B, let q:1B Aq: 1 \to B^A name the composite map

AδA×Aϕ×1 AB A×AevalBfBA \stackrel{\delta}{\to} A \times A \stackrel{\phi \times 1_A}{\to} B^A \times A \stackrel{eval}{\to} B \stackrel{f}{\to} B

from AA to BB. In lambda calculus notation, q=λa:A.fϕ(a)(a)q = \lambda a: A. f \phi(a)(a). Let p:1Ap: 1 \to A lift qq. Then calculate

ϕ(p)(p)=q(p)=(λa:A.fϕ(a)(a))(p)=fϕ(p)(p)\phi(p)(p) = q(p) = (\lambda a: A. f \phi(a)(a))(p) = f \phi(p)(p)

where the last equation is a beta-reduction. Hence sϕ(p)(p)s \coloneqq \phi(p)(p) is a fixed point of ff.

Remark

As pointed out by Lawvere, a hypothesis even weaker than point-surjectivity will do. Namely, g:XY Ag: X \to Y^A is called weakly point-surjective iff for every f:AYf: A \to Y there is x:1Xx: 1 \to X such that for every a:1Aa: 1 \to A, we have g(x)(a)=f(a)g(x)(a) = f(a). (This is weaker because g(x)=fg(x) = f cannot be inferred from g(x)(a)=f(a)g(x)(a) = f(a) for all global elements aa.)

Remark

The statement need not hold if “(weakly) point-surjective” is replaced by “epimorphism”. For example, in the cartesian closed category of compactly generated Hausdorff spaces and continuous maps, with S=S 1S = S^1 the circle, the Polish space S S^\mathbb{N} is compactly generated under the product topology; this is the exponential where \mathbb{N} is given the discrete topology. There is a countable dense subspace i:S i: \mathbb{N} \to S^\mathbb{N}, but recall that for any full subcategory of the category of Hausdorff spaces, a map f:XYf: X \to Y is an epimorphism iff it has a dense image. On the other hand, there are obvious rotations of SS that have no fixed points.

Thus epimorphisms need not be (weakly) point-surjective. Nor are point-surjective maps necessarily epimorphisms; for example, if UVU \hookrightarrow V is a proper inclusion between proper subobjects of the terminal object 11 (as may happen in a sheaf topos), then this is vacuously point-surjective but not an epimorphism.

Point-surjectivity may seem like an inadequate notion of “epimorphism”, but it suffices for many purposes. For example,

Proposition

(Cantor’s theorem in a topos) For any object XX, there is an epimorphism f:XΩ Xf: X \to \Omega^X only if the topos is degenerate.

Proof

Suppose there existed such an epi. In a topos, a map f:XYf: X \to Y is epi iff the direct image map f:Ω XΩ Y\exists_f: \Omega^X \to \Omega^Y retracts the inverse image map Ω f:Ω YΩ X\Omega^f: \Omega^Y \to \Omega^X, i.e., fΩ f=1 Ω Y\exists_f \circ \Omega^f = 1_{\Omega^Y}. Putting Y=Ω XY = \Omega^X, the supposition implies that f:YΩ Y\exists_f: Y \to \Omega^Y is a retraction. But retractions are automatically point-surjective.

We then conclude from Lawvere’s fixed point theorem that every endomorphism on Ω\Omega, in particular the negation ¬:ΩΩ\neg: \Omega \to \Omega, has a fixed point p:1Ωp: 1 \to \Omega. Then 0=p¬p=pp=p0 = p \wedge \neg p = p \wedge p = p, whence ¬0=0\neg 0 = 0, or “true = false”: the topos is degenerate.

Once we have a proposition pp with p=¬pp = \neg p, another way to conclude the proof is to apply Lawvere’s fixed-point theorem again to the surjection p0 pp \to 0^p, where pp is regarded as a subsingleton and 00 is the initial object, so that 0 p=¬p0^p = \neg p. This gives a fixed point 101\to 0 of the identity map 000\to 0, which again makes the topos degenerate. (The shorter version above is a beta-reduction of this.) For a formalization of this argument and a generalization thereof to universe types, see Escardo18.

Remark

Another version of Lawvere’s fixed-point theorem requires only finite products for its statement. Namely, in a category with finite products, suppose Φ:A×AB\Phi: A \times A \to B is a morphism with the property that for each g:ABg: A \to B there exists a:1Aa: 1 \to A such that gλ=Φ(a×1 A)g \lambda = \Phi \circ (a \times 1_A), where λ:1×AA\lambda: 1 \times A \stackrel{\sim}{\to} A is the projection. Then every map f:BBf: B \to B has a fixed point. This version of the theorem is emphasized by Yanofsky.

Remark

Many applications of Lawvere’s fixed point theorem are in the form of negated propositions, e.g., there is no epimorphism from a set to its power set, or Peano arithmetic cannot prove its own consistency. However, there are positive applications as well, e.g., it implies the existence of fixed-point combinators in untyped lambda calculus.

History

In an interview (Lawvere 07) not long after Gödel’s 100th birthday, William Lawvere answered the question

We have recently celebrated Kurt Gödel’s 100th birthday. What do you think about the extra-mathematical publicity around his incompleteness theorem?

by saying (reproduced in Lawvere 69 reprint, p. 2):

In ‘Diagonal arguments and Cartesian closed categories’ (Lawvere 69) we demystified the incompleteness theorem of Gödel and the truth-definition theory of Tarski by showing that both are consequences of some very simple algebra in the Cartesian-closed setting. It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a “paradox” by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science. Now, one hundred years after Gödel’s birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.

References

The original article:

  • William Lawvere, Diagonal Arguments and Cartesian Closed Categories, Lecture Notes in Mathematics, 92 (1969) 134-145 [tac:15]

Review and further development:

Exposition:

Formalization in Agda

The necessary assumptions for Lawvere’s account are reduced in various ways in

Last revised on August 10, 2023 at 11:58:15. See the history of this page for a list of all contributions to it.