Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Subobjects in elementary toposes

Morgan Rogers (he/him) (Sep 01 2026 at 15:32):

I was reading @Lingyuan Ye and @Yiqi Xu 's preprint and with the help of @Quentin Schroeder have managed to digest it a little. Since I don't have a blog etc, I thought I would share what I figured out here.

Context: Pitts asked in a paper published last year whether every Heyting algebra is realised as the lattice of subterminal objects in some elementary topos, and this paper provides an explicit counterexample.

In an elementary topos, we are a priori only allowed finitary operations. In particular, infinite unions or colimits need not exist. However, we are allowed some higher-order operations, and the key insight for understanding Lingyuan and Yiqi's paper is that these higher-order operations sometimes provide objects that happen to satisfy the universal property of a countable colimit, and thus that some infinite unions are required to exist in the lattice of subterminal objects.

Let $U$ be some object of our elementary topos equipped with a global element $u_0: 1 \to U$ and an endomorphism $S: U \to U$. In the paper they define a predicate $\mathsf{Reach}: U \to \Omega$ via the formula
$\forall Q: \Omega^U. \; \left(Q(u_0) \wedge (\forall v:U. \; Q(v) \rightarrow Q(Sv)) \right) \rightarrow Q(u).$
That is, $\mathsf{Reach}(u)$ holds to the extent that for all predicates $Q$ on $U$, $Q(u)$ can be proved inductively from $Q(u_0)$.

That formula looks like the induction principle for the natural numbers, and indeed we can show that the subobject it classifies inherits the operations from $U$, so it is almost a natural number object, except that there is no reason that the sequence $u_0,S(u_0),SS(u_0),\dotsc$ should be disjoint global elements of $U$, so this object may not have the initial coalgebra universal property.

Nonetheless, if we consider a predicate $Z:U \to \Omega$, then we have a sequence of global predicates $z_n := Z(S^nu_0): 1 \to \Omega$. They construct the global predicate
$\exists u:U. \; \mathsf{Reach}(u) \wedge Z(u) : 1 \to \Omega$
and show that this has the universal property of the countable union $\bigvee_{n \in \mathbb{N}} z_i$. So that union must exist!

The hard part (which I hope will be simplified in future iterations of their work!) is constructing a situation where the join in question provably does not exist in the chosen Heyting algebra of subterminals, which yields a contradiction. They do so in the free Heyting algebra on two generators.

I suspect that in this case the subobject defined by $\mathsf{Reach}$ is a natural number object, in which case the counterexample would simplify substantially, since countable unions are already required to exist in a topos with a natural number object, and it would be enough to already know they don't exist in the Heyting algebra; this could also lead to a more substantial negative result.
Anyway, I'm hoping the authors will correct me if I have made any technical errors :)

Nathanael Arkor (Sep 01 2026 at 16:22):

To provide a little more historical context: Pitts originally studied the question answered in the recent preprint over 30 years ago. It was what led to his 1992 On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. So this question has been open since at least then. (I would suggest the authors cite Pitts' earlier paper for the original context, and not just Pitts' recent talk slides.)

David Wärn (Sep 02 2026 at 14:46):

I suspect that in this case the subobject defined by $\mathsf{Reach}$ is a natural number object

It's worth keeping in mind that the external picture is very different from the internal one. Externally, the authors build a countable antichain $z_i$ in $\Omega$, so in particular all the $z_i$ are pairwise distinct when viewed as global truth values. Internally, these truth values are not pairwise distinct; indeed it is impossible to have three pairwise distinct truth values. Similarly in the internal language, $\Omega^6$ cannot have more than $2^6$ distinct elements, so it cannot have an embedding from an NNO.

David Wärn (Sep 02 2026 at 14:56):

Other than this I like your summary! I believe one can also phrase Lingyuan and Yiqi's result as saying that in an elementary topos, there is a certain map $F : \Omega^2 \to \Omega$, i.e. a binary operation on truth values, which does not arise from Heyting algebra operations. And they use something like an infinite join to define $F$.

Morgan Rogers (he/him) (Sep 02 2026 at 15:06):

@David Wärn could you say what it means precisely that one cannot internally have three pairwise distinct truth values? I think I understand intuitively why $\Omega^6$ is too small to contain a natural number object, but I can't immediately see what the formal statement is.

David Wärn (Sep 02 2026 at 16:04):

The following is a tautology of intuitionist logic: $\neg ( \neg(p \leftrightarrow q) \wedge \neg (p \leftrightarrow r) \wedge \neg (q \leftrightarrow r) )$. To prove this, note that this is a negated statement, so you may suppose $p \vee \neg p$, since $\neg \neg (p \vee \neg p)$ holds, and similarly with $q, r$. From there the proof is simple.

Yiqi Xu (Sep 02 2026 at 16:19):

@Morgan Rogers (he/him) Many thanks for this generous summary and for your interest in our paper. Apologies for not seeing your question sooner, I have not been able to check Zulip regularly.

Morgan Rogers (he/him) said:

I suspect that in this case the subobject defined by $\mathsf{Reach}$ is a natural number object, in which case the counterexample would simplify substantially, since countable unions are already required to exist in a topos with a natural number object, and it would be enough to already know they don't exist in the Heyting algebra; this could also lead to a more substantial negative result.

Unfortunately, $\mathsf{Reach}$ is not a NNO, or more precisely, the induced pointed endomorphism $(R,u_0,S|_R)$ is not a natural number object, where $R\hookrightarrow \Omega^6$ is the subobject classified by $\mathsf{Reach}$. The formula defining $\mathsf{Reach}$ gives an induction principle, but this is weaker than the recursion, or initial-algebra, property of an NNO.

The obstruction is local rather than global. Although the iterates $u_n$ are distinct as global sections, they are not internally disjoint. For every finite stage $K_{2,d}$, let $\kappa_d\neq\bot$ be the corresponding truth value. Since $K_{2,d}$ is finite, only finitely many restrictions of the $u_n$ to $\kappa_d$ can occur. Hence there are distinct $m,n$ such that

$\kappa_d\leq\llbracket u_m=u_n\rrbracket .$

In fact, a direct check on $K_{2,0}$ already gives

$\kappa_0\leq\llbracket u_2=u_3\rrbracket .$

Thus two distinct putative numerals coincide over a nonzero subterminal. This cannot happen in an NNO, in which distinct numerals have equality truth value $\bot$. This finite-stage local collapse is precisely what the predicates $I_d$ exploit in the hard direction of the proof.

Yiqi Xu (Sep 02 2026 at 16:26):

Nathanael Arkor said:

To provide a little more historical context: Pitts originally studied the question answered in the recent preprint over 30 years ago. It was what led to his 1992 On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. So this question has been open since at least then. (I would suggest the authors cite Pitts' earlier paper for the original context, and not just Pitts' recent talk slides.)

Many thanks for pointing this out. We have in fact included a citation to Pitts’s 1992 paper in the forthcoming revision.

Sridhar Ramesh (Sep 02 2026 at 16:44):

I notice the paper mentions the results were obtained with help from ChatGPT. Out of curiosity (trying to calibrate my understanding of this new era of math we are entering), what was the level of ChatGPT contribution? Did it come up with the main idea, or was it a tool for working out some fiddly technical details, or what should I make of it?

Nathanael Arkor (Sep 02 2026 at 16:47):

@Yiqi Xu: if I could make one more suggestion, I think that many people would be interested in knowing to what extent ChatGPT aided in finding the counterexample. E.g. whether it helped with one of the technical lemmas, or whether it came up with the entire counterexample and proof. The result is impressive regardless, but at the moment it is unclear which part of the contribution is entirely human and which is computer-assisted.

Nathanael Arkor (Sep 02 2026 at 16:48):

(Sridhar beat me to it :) )

Lingyuan Ye (Sep 03 2026 at 02:05):

Thanks @Morgan Rogers (he/him) for mentioning our paper here. Due to some personal issue I don't have enough time to respond fully currently, but I think @David Wärn 's comment (thanks!) and what @Yiqi Xu said should have explained the question.

Lingyuan Ye (Sep 03 2026 at 02:06):

@Nathanael Arkor @Sridhar Ramesh We have indeed added a section explaining our process of the interaction with AI, and hopefully the new version will come out soon.

Yiqi Xu (Sep 04 2026 at 06:45):

@Nathanael Arkor @Sridhar Ramesh We have posted a new version of our paper on arXiv. The final section gives a detailed account of how we worked with ChatGPT. Comments are very welcome.

Nathanael Arkor (Sep 04 2026 at 09:15):

Thanks, that's perfect!

Nathanael Arkor (Sep 25 2026 at 06:47):

For those interested, there's a new preprint on arXiv today by Zoltan A. Kocsis giving an alternative/modified proof: Two applications of the point-free coderivative.

Zoltan A. Kocsis (Z.A.K.) (Sep 25 2026 at 06:49):

Thanks @Nathanael Arkor, I'll be here later today to give a rundown

David Michael Roberts (Sep 25 2026 at 07:24):

Oh, cool! I was thinking about what the Cantor-Bendixson rank might be for locales in the not too distant past

David Michael Roberts (Sep 25 2026 at 07:27):

There was a preprint in HAL that never got published that sparked my interest and it made me think of doing that stuff again in a nice categorical way, and pointfree

Morgan Rogers (he/him) (Sep 25 2026 at 08:13):

Ooh I've been working with Cantor-Bandixson recently, I look forward to reading about the point free version!

Zoltan A. Kocsis (Z.A.K.) (Sep 25 2026 at 08:51):

So, regarding my preprint above.

My proof is a variant of Xu and Ye's. It uses the ideas they came up with: embedding $F_2$ into Bellissima's algebra, and what their preprint calls the "finite-stage separation" argument, which is used to show that their candidate obstruction term is indeed an obstruction term.

My variant only modestly simplifies this finite-stage separation argument. But it does replace $\theta$ with a different, conceptually simpler obstruction. This eliminates most of what @Morgan Rogers (he/him) called the "hard part" upthread: in particular, it gets rid of the sixfold $X,X',Y,Y',R,R'$ construction entirely.

Zoltan A. Kocsis (Z.A.K.) (Sep 25 2026 at 08:55):

Here's a summary of the argument:

The following operator $\nabla : H \rightarrow H$ is Simmons' point-free Cantor-Bendixson coderivative:

$$\nabla(y) = \bigwedge_{x \in H} (x \vee (x \rightarrow y)).$$

It is well-defined in any complete Heyting algebra $H$, but generally (in infinite algebras) cannot be written as a finite combination of the usual Heyting algebra operations $(\vee,\wedge,\rightarrow)$.

Bellissima embeds the free Heyting algebra on two generators, $F_2$, into a complete Heyting algebra $\mathfrak{H}_2$. So let $a,b \in F_2$ denote the free generators of $F_2$, and $\langle a \rangle, \langle b \rangle \in \mathfrak{H}_2$ the corresponding images in Bellissima's algebra. Using the fact that $\nabla$ is the coderivative, one can then show that $\nabla \langle a \rangle$ is not the embedded image of any element in $F_2$.

Assume for a contradiction that $\mathcal{C}$ is a topos whose truth value algebra is isomorphic to $F_2$. This means that we can associate the truth value of every sentence (closed formula) in the internal language of $\mathcal{C}$ to some element of $\mathfrak{H}_2$ via the Bellissima embedding.

Under these assumptions, one can prove that the truth value of the sentence

$$\forall x: \Omega.\: \mathrm{Gen}(x) \rightarrow (x \vee (x \rightarrow a))$$

would have to map to $\nabla \langle a \rangle$ under the Bellissima embedding. This is impossible, since $\nabla \langle a \rangle$ is not the embedded image of any element in $F_2$.

Here, $\mathrm{Gen}(x)$ denotes the following internal statement:

$x$ belongs to every Heyting subalgebra $S \subseteq \Omega$ that contains $a$ and $b$.

Apart from the new obstruction term, the resulting proof follows the original argument of Xu-Ye fairly closely and has the same external prerequisites. But I think this simplifies the proof enough that one can explain it in full detail in one go. I'll try to write such a longer walkthrough tomorrow, starting from how I think about Bellissima's construction, probably in an Our work thread. There I'll also explain why we definitely need $\mathrm{Gen}(-)$, and why taking just

$$\forall x: \Omega.\: x \vee (x \rightarrow a)$$

as the obstruction term cannot work.

Zoltan A. Kocsis (Z.A.K.) (Sep 25 2026 at 08:57):

Huge congratulations to Lingyuan and Yiqi: fwiw I checked every step of their proof while I worked this out, and am really quite confident it's all correct. It's a really nice result, and it was fun to play with their ideas.

David Michael Roberts (Sep 25 2026 at 09:50):

And it turns out that Simmons essentially did a bunch of what I was considering, years ago!

Valeria de Paiva (Oct 03 2026 at 03:01):

Harold Simmons was a great guy! I'm happy to see his work showing up again.

Morgan Rogers (he/him) (Oct 03 2026 at 07:00):

He wrote an introduction to category theory that is much less well-known than some others but which I learned a great deal from.

John Baez (Oct 03 2026 at 09:56):

What's it like? In particular, how is it different from others? I've never heard of it!

Valeria de Paiva (Oct 03 2026 at 18:50):

well the book is from 2011 and the blurb says: Category theory provides a general conceptual framework that has proved fruitful in subjects as diverse as geometry, topology, theoretical computer science and foundational mathematics. Here is a friendly, easy-to-read textbook that explains the fundamentals at a level suitable for newcomers to the subject. Beginning postgraduate mathematicians will find this book an excellent introduction to all of the basics of category theory. It gives the basic definitions; goes through the various associated gadgetry, such as functors, natural transformations, limits and colimits; and then explains adjunctions. The material is slowly developed using many examples and illustrations to illuminate the concepts explained. Over 200 exercises, with solutions available online, help the reader to access the subject and make the book ideal for self-study. It can also be used as a recommended text for a taught introductory course.

• No knowledge assumed beyond what any beginning postgraduate should know
• Exercises and solutions enable the individual learner to test their own understanding
• Solutions to all exercises at www.cambridge.org/simmons

Morgan Rogers (he/him) (Oct 04 2026 at 09:42):

I particularly appreciated that it covered posets and monoids as special cases of categories from first principles i.e. not assuming that the reader has any experience working with these.

Sam van G (Oct 06 2026 at 12:49):

Hi all, I've just posted a note in which I try to explain my understanding of the proof(s) of this theorem, accompanied by a version with links to a Lean formalization. Thanks to several people here for discussions about this, see also the acknowledgments in the pdf.