The n-Category Café

Regarding Dedekind, he wrote down a proof of the result without choice while in the later stages of drafting Was sind und was sollen die Zahlen? (in July 1887), but didn’t include it in that monograph. However, he did include a related result which essentially gives it to you, using a very similar method of proof - and it is (I think) the only statement not explicitly proved in that text, and left to the reader. As you say, this was in the middle of the period with a strained relationship with Cantor.

For those who are interested, Arie Hinkis’ book Proofs of the Cantor-Bernstein Theorem digs into the history.

Wow, David, that’s an amazingly comprehensive book! What a labour of love. Thanks for linking to it; I had no idea it existed.

It’s also free through the link David gives.

I’d like to sit in your class and hear you tell that story about the envoys!

I don’t deny that there’s a lot of categorical thinking going on in this course on sets (even though I don’t mention categories), just as there may be a lot of ring-theoretic thinking going on in a course on number theory (even if they never mention rings).

I hope the students will find that a good deal of what they learn is useful for other subjects too. It’s not my primary purpose to teach them generally useful stuff, but I do think it’s a substantial fringe benefit of a categorical approach (even a secretly categorical approach) that you learn more broadly applicable concepts than you do in a ZFC-based course.

However, with each week that passes, the course does feel more particular to sets and less about general categorical notions. For example, last week’s proof of Cantor’s theorem on $X \lt P(X)$ and the Cantor–Bernstein theorem are highly specific to sets. General categorical thinking won’t help you much there.

What we’re doing this week (in notes I’ll release soon) is the definition and structure of $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ and $\mathbb{R}$. The material on $\mathbb{N}$ inevitably starts off by using the axiom that there exists a natural numbers object. But pretty soon in the development, everything starts looking just about the same as in any other axiomatization of set theory.

The topics for the remaining weeks are well ordered sets, the axiom of choice, and cardinal arithmetic. This will be really very close to the development that you’d see in a ZFC-based course. The main difference is that everything will be isomorphism-invariant — so, no transitive sets etc. But the results are essentially all the same.

I also wonder if the amount of category theory is actually necessary for ETCS and I suspect it mostly is.

I’ve tried to keep the generalities to a minimum. That doesn’t mean I’ve succeeded: I’m not naturally a concise writer, and these notes are a first iteration written under great time pressure. Plus, while I did detailed advance planning of the whole course, I’m not one hundred percent sure which results I have to include in earlier chapters in order to be able to use them in later chapters. So there’s probably some fat that could be trimmed, despite my best efforts.

Dr. Kirby

You write:

“I also wonder if the amount of category theory is actually necessary for ETCS and I suspect it mostly is.”

There is a reason for this which is obscured in “a battle of set theories” (Dr. Shulman’s material/structural distinction). The debates which had occurred on the FOM mailing list between Dr. Friedman and category theorists had been about advocacy over the first-order paradigm — not “sets.” When one reads Lawvere and Rosebrugh, the significant element of category diagrams for reconstruction of “set intuition” are inclusions. Historically, one may compare this with more modern accounts of the mereological part relations.

Where Lawvere and Rosebrugh elevate Dedekind and criticize philosophers, they ignore Russell’s critique of Dedekind relative to Peano. Russell’s observations have been restated in “Set Theory and Its Philosophy” by Michael Potter.

In effect, inclusions approach “individuation” via singleton sets. This is how Zermelo had approached the idea in his 1908 paper (If I recall correctly, it also appears in Padoa’s paper where models for identifying axiom independence is introduced.). For Zermelo, this use of singleton sets appears motivated by a need to accommodate urelements. However, the logicist view of set theory had changed to an algebraic view with Skolem’s criticism of “definite properties” in Zermelo’s paper. First-order advocates will always object to conflation of “an individual” with the singleton having an individual as an element. And, this goes back to Russell’s comparison of Dedekind and Peano.

With Skolem, support for urelements becomes an axiom for a “set” of urelements (everything is a set) unnecessary for mathematics (a theory of pure sets suffices).

If one understands Lawvere’s contribution as a reverse engineering of symbolic logic, then one can have a deep appreciation for how “element” and “member” are interpreted by Lawvere. Along similar lines, where the status of “names” is central to the linguistic paraphrases of symbolic logic, the explanation of “names” in McClarty is equally impressive.

Once one acknowledges that the debate involves individuation and interpretation for the sign of equality, the two papers to compare are Lawvere’s paper on the unity of opposites

https://github.com/mattearnshaw/lawvere/blob/master/pdfs/1996-unity-and-identity-of-opposites-in-calculus-and-physics.pdf

and Russell’s rejection of “differences” on PDF page 7 of his paper “On Denoting,”

https://www.philosophy-index.com/russell/on-denoting/Russell-On_Denoting.pdf

For what this is worth, Russell’s view is useful to the verificationist perspective of homotopy type theory. It is implicit to the sequent axiomatization found in the guest post on identity types sponsored by Dr. Riehl. And there is a particularly unfortunate circumstance that makes this so difficult to sort out — logicism, first-order logic, and Herbrand logic share the same inference rules. So, when one portrays the situation as “a battle of set theories,” it is difficult to figure out who is arguing against what.

“The more I read of your notes, the more I wonder if it is really a course in category theory or in set theory.”

It’s a course in set theory. A course on category theory will inevitably talk about functors and adjunctions and natural transformations and general limits/colimits and the Yoneda lemma and those are completely missing from this course.

Well, it’s “Paré’s … construction of colimits in a topos.” that Tom described as sublime, not the construction of a disjoint sum.

And why are you assuming that the word “trick” here is being used in a deliberately disparaging way? (Tom is not Lawvere, for instance) Do you think ‘Scott’s Trick’ is a belittling term? Getting the construction of disjoint sum as a special case from the monadicity of contravariant powerset is a rather nice thing to know, regardless of one’s preference for foundations.

The method I called a trick is more or less the one I chose to use in my course. I chose to use it because it’s the argument I liked best in the context. That doesn’t stop me from also finding Paré’s construction beautiful.

Not everything has to be a war.

I can’t resist summarizing Paré’s argument for those who haven’t seen it before — in which case, you’re in for a treat. The theorem is that every (elementary) topos has finite colimits. Paré wasn’t the first to prove this, but he found the following wonderful proof.

For any topos $\mathcal{E}$, the contravariant power set functor $P: \mathcal{E}^{op} \to \mathcal{E}$ is self-adjoint on the right. That is, maps $X \to P(Y)$ correspond to maps $Y \to P(X)$. This is because $P = \Omega^{(-)}$, and so a map $X \to P(Y)$ is the same thing as a map $X \times Y \to \Omega$, which is the same as a map $Y \times X \to \Omega$, which in turn is the same as a map $Y \to P(X)$.

Better still, this adjunction is monadic. This can be proved using the monadicity theorem. Hence the functor $P: \mathcal{E}^{op} \to \mathcal{E}$ is monadic. But monadic functors create limits! And since $\mathcal{E}$ has finite limits, $\mathcal{E}^{op}$ has finite limits too — that is, $\mathcal{E}$ has finite colimits. Isn’t that wonderful?

If you unwind this general proof and specialize to the case of binary coproducts in the topos of sets, then you eventually end up with the following: $P(X + Y)$ is constructed as $P(X) \times P(Y)$, and $X + Y$ is constructed as the set of singletons in $P(X + Y)$. Putting these together gives a construction of $X + Y$ as a subset of $P(X) \times P(Y)$, namely, the subset in the second display of James’s comment (where $X$ and $Y$ are called $A$ and $B$). Of course, what people find so elegant about Paré’s argument is the general proof by monadicity that all toposes have all finite colimits, not the particular formula that can be extracted in this special case.

I really don’t want to spend time arguing about a single word I used in an off-the-cuff blog post two months ago. “Trick” isn’t necessarily pejorative; I’m thinking here of the Tricki project of Tim Gowers and collaborators (a compendium of their favourite tricks), and the critical role played by the tensor power trick in my last book, and this MO question on “every mathematician has only a few tricks”, and, as David mentioned, Scott’s trick. There’s a famous quote attributed to Pólya along the lines of “an idea used once is a trick; an idea used twice is a method”; whether one sees something as a trick depends on whether one sees it as fitting into a larger framework, which is quite subjective.

Back to the mathematics. The three constructions we’re talking about do three different things:

• Paré’s construction gives arbitrary finite colimits in an arbitrary topos.

• The construction in my notes gives disjoint unions in an ETCS category.

• The usual ZFC construction gives disjoint unions in a model of ZFC (where, in contrast to the other two settings, taking the union of an arbitrary pair of sets is a well-defined operation).

For anyone reading this who hasn’t looked at the relevant part of my notes (i.e. almost anyone reading this :-) ), what I did was the following.

A disjoint union of sets $X$ and $Y$ is defined to be a set $D$ together with injections $X \to D \leftarrow Y$ such that every element of $D$ is mapped to by either an element of $X$ or an element of $Y$, but not both. I showed that $X$ and $Y$ always have a disjoint union in three steps:

• First, there’s some set $Z$ into which $X$ and $Y$ both embed, but perhaps not disjointly. (If $X$ or $Y$ is empty, you can take $Z$ to be $Y$ or $X$; assuming otherwise, you can take $Z = X \times Y$.)

• From this, it follows that $X$ and $Y$ embed disjointly into $2 \times Z$. (Embed $X$ into the first copy of $Z$ and $Y$ into the second.)

• Then take the union of the images of these two disjoint embeddings to get a disjoint union $D$.

And it’s then proved that disjoint unions are coproducts. Concretely, this means that casewise definitions of functions are legitimate (e.g. define $f(x)$ in one way if $x \geq 0$ and in another if $x \lt 0$).

The splitting off of the trivial cases in the first step isn’t ideal, for sure. I could have avoided that by replacing the first two steps by the Paré-style move of embedding $X$ and $Y$ disjointly into $P(X \times Y)$. I forget exactly why I preferred not to, but surely for pedagogical reasons, perhaps the reason you mention: using something as big as a power set just to build a coproduct seems like overkill.

One other aspect of Paré’s construction that I enjoy is what happens if you specialize it to coequalizers in $Set$, and in fact specialize even further to quotienting a set $X$ by an equivalence relation $\sim$. The recipe for $X/{\sim}$ that pops out of Paré’s proof in this case is precisely the same as the standard first-year undergraduate one: it’s the subset of $P(X)$ consisting of the equivalence classes. So what might seem like an isolated idea, that you can construct the quotient $X/{\sim}$ as a set of subsets of $X$, appears here as part of a bigger story.

(But again, in my course I didn’t tell that story: I just constructed $X/{\sim}$ directly as a set of equivalence classes.)

Having said how much I appreciate Paré’s argument, I do think there’s something a bit odd about the theorem that toposes have finite colimits. It’s a bit like starting with multiplication and exponentiation on $\mathbb{N}$ and constructing addition from them, when the usual approach is the other way round. I guess the Paré-style argument would be like this: given natural numbers $x$ and $y$, somehow show that there’s a unique number $x + y$ such that $2^{x + y} = 2^x \cdot 2^y$.

If my memory doesn’t betray me, someone — maybe Todd Trimble — told me that Lawvere and/or Tierney and/or Schanuel contemplated finding an approach to toposes where colimits rather than limits were given the central role. I guess this is related to Lawvere and Schanuel’s work on extensive categories, but as far as I know the full idea has never been brought to fruition.