How to be concrete when you don’t have a choice

I forgot to write a post about this a year ago, but I gave a talk at AustMS2020 detailing some work that Martti Karvonen and I did, originating in a discussion on the category theory Zulip chat server. The main gist of the project is removing the need for Global Choice from a pair of theorems in pure category theory dealing with concrete and non-concrete categories. The most famous example (shown by Freyd) of a non-concrete locally small category is the homotopy category of \mathbf{Top}, which is the category whose objects are topological spaces, but whose morphisms are homotopy classes of continuous maps. It is a quotient of the concrete category of topological spaces, by a congruence on its hom-sets. The first theorem that we improved, due to Kučera, is that this is as bad as it gets: every locally small category is the quotient of a concrete category by a congruence like this. The proof constructs a concrete category, but it’s not very nice or workable, so it’s really just an existence result.

Unfortunately the original proof starts by well-ordering the universe of sets, which really makes me itch: category theory is generally rather constructive in nature, or at least can be reformulated to have some kind of constructive content. A purely category-theoretic statement that needs the axiom of Global Choice seems non-optimal to me. And, thankfully, this is the case. Martti came up with a way to remove Choice (even normal AC) from the construction, and then I figured out how to do the whole thing in Algebraic Set Theory with the assumption of Excluded Middle (i.e. the category with class structure is Boolean).

Then we turned out attention to a theorem of Freyd that gives a precise characterisation of which categories are concretizable, albeit we started from Vinárek’s cleaner and shorter proof. It shows that a necessary condition for concreteness, due to Isbell, is also sufficient. Isbell gave examples of non-concretizable categories, but they were artificial, specifically constructed to violate his condition. Like Kučera’s theorem, even Vinárek’s improved proof used Global Choice to pick a well-ordering of the universe. We were able to re-do the theorem in ZF, and more generally in (Boolean) algebraic set theory, with the additional assumption that the universal object has a well-ordered stratification by small objects (roughly, it has a small map to the object of ordinals). This last assumption is validated in any membership-based set theory where some cumulative hierarchy exhausts the class of all sets, say the von Neumann hierarchy for ZF, or some weaker set theories where a hierarchy, or a rank function, is posited axiomatically (see eg this paper).

The paper is in preparation, and would have been done by now, had I not been distracted by other projects. Martti is being very patient with me! For now, let me point to the slides for my talk, which you can see here.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.