The n-Category Café

Number 10 in Tom’s list is a version of the axiom of choice, so removing that (probably?) gives you ZF.

While not topos theoretic (as the theory forms a bicategory of relations rather than a well-pointed topos), Mike Shulman’s SEAR is a neutral/categorical set theory that is equiconsistent with ZF. I am not sure if SEAR is biinterpretable with ZF.

It’s certainly true that from a model of any membership-based set theory you can construct a model of the corresponding categorical set theory and vice versa; I wrote about this at length for a lot of weaker set theories in Comparing material and structural set theories. Intuitively I would call that “biinterpretable”, since if you can construct a model of theory 1 in theory 2, you can “interpret” theory 1 in theory 2 by interpreting it in that model. Does “biinterpretable” have a fancy meaning other than this obvious one?

I’m glad you’re looking forward to the rest, but I suspect it will mostly be stuff you already know well… anyway, let’s see!

I agree about the importance of well-ordered sets. To me, this has been one of the most interesting aspects of the whole exercise: not throwing out the baby with the bathwater.

One point that will come up in a later post is the adjunction between sets and well-ordered sets. What I mean is this.

• Let $\mathbf{WOSet}$ be the category whose objects are well-ordered sets and whose maps are order-embeddings with downwards closed image (i.e. embeddings as an initial segment). The category $\mathbf{WOSet}$ is actually a preorder; I’ll write $V \preceq W$ to mean that there exists a map $V \to W$ in $\mathbf{WOSet}$.

• Let $\leq$ be the relation on sets defined by $X \leq Y$ iff there exists an injection $X \to Y$. Then $(\mathbf{Set}, \leq)$ is also a preorder.

• There is a forgetful functor $U: (\mathbf{WOSet}, \preceq) \to (\mathbf{Set}, \leq)$, since an order-embedding is in particular injective.

• There is a functor $I: (\mathbf{Set}, \leq) \to (\mathbf{WOSet}, \preceq)$ defined by taking $I(X)$ to be $X$ equipped with a well-ordering that’s initial (i.e. $I(X) \preceq W$ for any other well-ordered set $W$ with underlying set $X$).

Then $I$ is left adjoint to $U$:

$$I(X) \preceq W \iff X \leq U(W)$$

for every set $X$ and well-ordered set $W$. Since $U \circ I \cong id$, this adjunction restricts to an equivalence between sets and initial well-ordered sets. And that gives the “possible structural meaning of ‘cardinal’” that you started with in your comment.

What I meant about babies and bathwater is that it does seem to me that the equivalence between sets and initial well-ordered sets is significant. Sometimes we have a choice about whether we use it or not (e.g. you can define the cofinality of a set directly or via the corresponding WO set). But sometimes the equivalence, or the entire adjunction, seems pretty much essential.

A sign that quotienting as a higher inductive type (HoTT book, 6.10) prevails?

Interesting, I didn’t know about that usage of “representation”.

Actually, for the post I wrote and then deleted a paragraph contrasting parts of mathematics where there are multiple relevant notions of isomorphism and parts where there are only one. It seems to be a geometry/algebra divide.

In geometry, you have diffeomorphism, homeomorphism, homotopy equivalence, birationality, etc., so we do more often need to say things like “homotopy type”, “birationality class”, etc.

But in algebra, there usually seems to be only one sensible notion of isomorphism (though I’m sure there are exceptions). That means we can get away with just saying “group” etc. without having to specify what it’s “up to”.

Morita equivalence would be one example I suppose.

You’re absolutely right. As I was writing the post, I realized there was something to be resolved here, but I opted for going ahead and posting rather than agonizing over it.

What I think I mean is this. There’s ETCS, which will be the formal axiom system I’m using. Then there’s the way I’m going to write about ETCS. My intention is to write neutrally.

I think what this means is that implicitly, I’ll be using the following set theory — let’s call it $\in$TCS. It’s very much like ETCS, but with the following differences.

The primitive concepts of ETCS (as I’m presenting it) are sets, functions $X \to Y$ for each set $X$ and set $Y$, composition, and identities. For $\in$TCS, we take the same primitive concepts and two more:

• For each set $X$, some things called elements of $X$, writing $x \in X$ to mean that $x$ is an element of $X$.

• For each set $X$, set $Y$, function $f: X \to Y$ and element $x$ of $X$, an element of $Y$ called the evaluation of $f$ at $x$ and written as $f(x)$.

The axioms of $\in$TCS are very similar to those of ETCS, but with the following additions.

• Given an element $x \in X$ and functions $f: X \to Y$ and $g: Y \to Z$, we require that $(g \circ f)(x) = g(f(x))$.

• Given an element $x \in X$, we require that $\id_X(x) = x$.

• A set is terminal if and only if it has exactly one element.

• For every terminal set $1$ and element $\star$ of $1$, and for every set $X$ and element $x$ of $X$, there is exactly one function $f: 1 \to X$ such that $f(\star) = x$.

I think that’s enough to guarantee that $\in$TCS is equivalent to ETCS in the strongest sense. Quite possibly I’ve added more axioms than necessary. One day I should work this out properly.

In any case, the point is that there’s some set theory $\in$TCS (either as I’ve just defined it or a variation) that’s equivalent to ETCS but has $\in$ as a primitive concept. That way, we don’t need to define an element of a set $X$ as a map $1 \to X$, even though there’s a one-to-one correspondence between the two things. My thought is that the “neutral” way I’ll be doing set theory in the coming posts is implicitly using $\in$TCS or something like it.

I am not entirely sure how important it will be in this series, but ETCS also has no way of representing indexed families of sets, which the material set theories like ZFC can. One would either have to include Grothendieck universes and define indexed families as functions into a universe, or directly include indexed sets into the primitives a làdependent type theory.

Ha, no, these “bigger things” have no connection to magnitude as far as I know!

One answer to your question is this:

My primary interest is not actually in large cardinals themselves. What I’m really interested in is exploring the hypothesis that everying in traditional, membership-based set theory that’s relevant to the rest of mathematics can be done smoothly in categorical set theory.

Another is more personal. I find it quite soothing to think about set theory. I find it especially soothing to think about set theory when I’ve been working on more applied or analytic things — it’s a pleasant contrast — or when there’s a pandemic starting. It’s a refuge.

At some point I started working through all the set theory I knew and figuring out how to do it using the categorical approach. Eventually I ran out of set theory I knew and had to learn some more. I’m not going to devote the rest of my life to learning more set theory and redoing it categorically, but I’ve enjoyed the part I’ve done.

:-)

Lots of comments are anticipating later parts of this series, which is great. Your comment, David, anticipates what I think will be almost the final post.

I’m not going to go any bigger than measurable sets. To a set theorist, this is still quite petite. E.g. Kanamori’s book The Higher Infinite dispenses with measurability in section 2 out of 32. But there’s lots interesting along the way from ETCS to measurability.

When I get to measurability, I’ll say something about the result of Isbell that Lawvere is alluding to here, and a variant of it involving a single object $V$ (in Lawvere’s notation).

I understand most of Lawvere’s comment, but I wonder what in algebraic geometry he’s thinking of here:

Various kinds of “measurable” cardinals arise as possible obstructions to simple dualities of the type considered in algebraic geometry.

I suppose he’s not quite saying that measurable cardinals arise as possible obstructions to simple dualities considered in algebraic geometry — he says of the type considered in algebraic geometry. If that “of the type” is a crucial part of the sentence, then it’s much less interesting and I suppose I can guess what he means. But if there is actually a duality in algebraic geometry that’s somehow obstructed by measurable cardinals, I’d like to hear what it is.

With Lawvere’s talk of “bornology” and “real compactness”, I wonder if there’s a whiff of condensedness in the air. Recall Peter Scholze told us that

If you wish, condensed sets are bornological sets equipped with some extra structure related to “limit points”, where limits are understood in terms of ultrafilters,

and it wouldn’t surprise me if your codensity monads were about here somewhere.

I’m not going to go any bigger than measurable sets.

I’m somewhat surprised that Vopěnka’s principle won’t be mentioned in the series, especially on a blog specifically dedicated to category theory.

Thank you, Emily!

The pedagogical practicality of such an effort might be reasonably questioned

It definitely might; it would be interesting to hear from one of his former students there. But I have to applaud a teacher who takes teaching seriously, responding creatively to a pedagogical challenge, rather than being a teaching bot doing same-old same-old (always an available option). Whatever the outcome for his students, we category theorists are grateful!

Thanks, Kyle! That episode is truly mind-boggling.

I can imagine putting something about each of the ETCS axioms into a first-year undergraduate course, though it wouldn’t be calculus and I’d have to soft-pedal many of the axioms.

And I can see some benefit in doing something like this. I used to teach the introductory general topology course in Edinburgh, and I noticed that even our best students (and some of them are excellent) tripped up on basic set-theoretic points — e.g. they had trouble seeing why, if $A, A' \subseteq X$ and $B, B' \subseteq Y$, the subset $$(A \times B) \cup (A' \times B') \subseteq X \times Y$$ needn’t be of the form $A'' \times B''$. The difficulty was not with the topology, it was with basic set theory. (A picture makes it clear, but they weren’t seeing that picture in their heads, or easily translating between pictures and algebraic formalism.) I found myself wishing they’d done more of that kind of set theory early on.

Similarly, a common point of difficulty for beginning algebra students is understanding quotient groups/rings. It seems to me that this is partly because the students are simultaneously having to understand a new set-theoretic thing (basically the universal property of the quotient of a set by an equivalence relation) and a new algebraic thing. It might be beneficial to teach the set-theoretic thing separately first.

I can just about imagine doing a proper formal version of the ETCS axioms in, say, a third year course at a Scottish university or a second year course at an English university. (Scottish students study more broadly, hence do less mathematics per year in the early years.) But it would take some doing. In actual reality, there may be an opportunity one day for me to teach axiomatic ETCS in a fourth year course here — but this is a long way from Lawvere’s original radical plan!

I’ve just been rereading Lawvere’s An elementary theory of the category of sets (long version) with commentary, where he relates some further recollections of what happened at Reed College. From p.5-6:

This elementary theory of the category of sets arose from a purely practical educational need. When I began teaching at Reed College in 1963, I was instructed that first-year analysis should emphasize foundations, with the usual formulas and applications of calculus being filled out in the second year. Since part of the difficulty in learning calculus stems from the rigid refusal of most textbooks to supply clear, explicit, statements of concepts and principles, I was very happy with the opportunity to oppose that unfortunate trend. Part of the summer of 1963 was devoted to designing a course based on the axiomatics of Zermelo-Fraenkel set theory (even though I had already before concluded that the category of categories is the best setting for “advanced” mathematics). But I soon realized that even an entire semester would not be adequate for explaining all the (for a beginner bizarre) membership-theoretic definitions and results, then translating them into operations usable in algebra and analysis, then using that framework to construct a basis for the material I planned to present in the second semester on metric spaces.

However I found a way out of the ZF impasse and the able Reed students could indeed be led to take advantage of the second semester that I had planned. The way was to present in a couple of months an explicit axiomatic theory of the mathematical operations and concepts (composition, functionals, etc.) as actually needed in the development of the mathematics.

Incidentally, I’ve never been able to think of a justification for that phrase

the rigid refusal of most textbooks to supply clear, explicit, statements of concepts and principles.

Sure, sometimes people don’t write clearly, but he’s obviously saying more than that. Refusal is a very strong word, as if the writers of calculus textbooks know how to make “concepts and principles” clear and explicit but choose not to.