Discussing "Sketches of an Elephant: A Topos Theory Compendium"

Links: Volume 1 and Volume 2

Author: Peter T. Johnstone (University of Cambridge)

Reference: Johnstone, Peter T., Sketches of an Elephant: A Topos Theory Compendium: Volume 1 and 2. Oxford University Press, 2002

Why this book? Cited by Groupoid-Valued Presheaf Models of Univalent Type Theory, KZ-monads and Kan Injectivity, and Classifying Topoi in Synthetic Guarded Domain Theory

The algorithm I follow to choose topics for this blog, where I take the most highly cited paper from my recent Google Scholar recommendations, can send me off to anything from a short conference paper to a full book. I like the variety, but of course a short blog post can only say so much about a book based on a week of reading pushed in around my other commitments; this was never more true than this week, given the monumental scale and density of these two volumes. The introduction even warns one off reading the book from start to finish; it is intended to be a tome one can dip into to find all manner of important facts in topos theory, including full proof details.

The title of the book refers to the ancient parable of the blind men and the elephant, where men touching different parts of the elephant come to different conclusions about its nature. The book is structured around sections describing the category theoretical notion of topos in different ways - as a category, as a 2-category, as a space, and as a logical theory (the latter being my main focus). The contents for a third volume are also included, covering homotopy / cohomology and mathematical universes, but more than twenty years later this is perhaps as likely to appear as the final Game of Thrones novels – but who knows?

The central definition of a topos in category theory is quite simple for something that can inspire so many pages of work, but this is in keeping with the usual nature of category theory – simple abstract definitions with many examples, which help to organise the structure of mathematical thought and provide connections between apparently unconnected areas. The distinctive concept here is that of subobject classifier, which can be seen as an object of ‘truth values’.  Classically, one can use the two element set of the Booleans True and False, but, to take a contrasting example, in the topos of trees the subobject classifier provides for an infinite-valued logic, as I discussed a few weeks ago. In any topos, the logic provided for by the subobject classifier is at least intuitionistic, but need not be classical (admitting the law of excluded middle, double negation elimination, and so on).

What do I mean by the ‘logic provided for’? To skip ahead to the logic section in the second half of the second book, a lot can be achieved without going all the way to toposes. For example, (sorted) first-order logic of the kind one might be taught in an introductory logic course can be interpreted in any Heyting category, which is a weaker definition than topos. The full power of toposes are not needed to interpret logical theories until one reaches for higher-order logic; in particular the ability to have variables ranging over subsets of a sort (more generally, type), and to sensibly use the set membership symbol ∈, requires the subobject classifier. Having said that, toposes do have their uses as an analytic tool before we get to such powerful logics, as each theory (collection of axioms) expressed with the weaker logics can be aligned to a ‘classifying topos’ which contains a universal model of the theory – a model that satisfies all and only the theorems entailed by the theory.

I should finish by mentioning one of the most stunning achievements of topos theory (to my mind; given the nature of the elephant a topologist would probably come up with something else), which is the connection of the notion of classical logic (certain toposes are Boolean, which means that their underlying logic will be classical) to the axiom of choice much discussed in mathematics. The results, rewarding one for getting 991 pages into the book (or skipping forward to them, as is more to be advised) give a description of Booleans toposes exactly in terms of the choice functions of certain of their objects, and, following Zermelo’s theorem, show that in any topos (including non-Boolean) the objects with choice functions are exactly those that are well-orderable. These results, and others around them, bring a remarkable new clarity to the connections between two of the most discussed concepts in the foundations of mathematics, classicality and choice.