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.
Martin Brandenburg (Aug 15 2026 at 19:37):In this thread I will share the releases of CatDat (announced here). Maybe I will write something from time to time. The complete list of releases is here.
Martin Brandenburg (Aug 15 2026 at 19:39):Release v1.18.0 adds support for symmetric monoidal categories, includes several refactorings, and introduces parent structures. See the release notes and the linked PRs for details. (I usually write very detailed PR descriptions.)
Parent structures are cool because once you prove something for, say, the category of R-modules, it automatically proves it for the category of abelian groups.
Martin Brandenburg (Aug 15 2026 at 19:53):While working on the properties of morphisms (here), I have created this nice overview. It is more detailed than the diagram in Joy of Cats. I haven't added it to the nLab because the editor always gives me errors (even though I have used exactly the same tikz syntax as on other pages).
For now, I have added these diagrams on this page. They are not finished; for example, (effective) descent morphisms are currently missing.
David Michael Roberts (Aug 16 2026 at 07:30):Can we put that epimorphism impliciation diagram on the nLab please, linking to CatDat for credit?
David Michael Roberts (Aug 16 2026 at 07:32):Maybe as an !include in all the pages for those flavours of epimorphisms? I usually have to go to [[epimorphism]] which has the list and the discussion of relations, but other pages in the hierarchy don't all list the ways in which they relate.
Martin Brandenburg (Aug 16 2026 at 08:02):David Michael Roberts said:
Can we put that epimorphism impliciation diagram on the nLab please [...]
Yes. But as mentioned, I have tried to do that (in fact, on the epimorphism page you mentioned), but I failed. An image would be easier, but (a) I don't know where to upload images for the nLab and if this is allowed at all, (b) an image cannot be edited, (c) so a tikzcd diagram would be better, but when I try to create any new tikzcd diagram on the nLab (even a simple one with just one node), the editor will throw an error.
Maybe someone else is more lucky than me? The tikzcd source code of the diagrams can be found here:
https://gist.github.com/ScriptRaccoon/132fea9d3487cdb42f77b11593592917
[...] linking to CatDat for credit
Actually, my plan is to do it the other way round. nLab for documentation, CatDat for barebones data. I want to delete the CatDat page with the overview (the implications are saved in the database already) and replace the links to it with links to the nLab page, once the diagrams are on the nLab.
I also saw Urs linking to the CatDat page on the category of abelian groups on this nLab page, but I don't like this since CatDat should rather refer to nLab, not vice versa.
David Michael Roberts (Aug 16 2026 at 11:02):OK, we can solve this, images on the nLab are fine, the tikz capacity on the nlab is practically non-existent. I'll get on this tomorrow
David Michael Roberts (Aug 16 2026 at 11:08):Sorry I somehow missed the bit where you said you'd tried already!
Martin Brandenburg (Sep 02 2026 at 15:40):Release v1.19.0 adds a technical example of a cocomplete category without equalizers (the free cocompletion of a suitable locally small category). Deciding all of its properties involved quite a lot of work. In this context, free cocompletions and small presheaves have also been studied in general. I was quite amazed to see that this example alone has witnessed 73 new combinations (!) of properties of the form "p and not q", or 153 when duals are taken into account.
Moreover, I have started to break down the property of being regular into its constituent properties by adding the properties of having kernel pairs and of having coequalizers of kernel pairs (and their duals). The PR for the property of having pullback-stable regular epimorphisms is already in progress.
The goal behind that is to have all constituents of a property in the database also recorded in the database. That is, if a property P is defined by "A and B and C are satisfied", we should try to add A, B, and C separately and record the equivalence P ⇔ A + B + C. Deciding A, B, and C for all categories in the database then gives a more detailed understanding of P, and in many cases, multiple proofs can be combined into one.
Furthermore, I realized that it would be better to distinguish between "natural number objects" and "parametrized natural number objects". Previously, only the latter was recorded, but without the "parametrized" prefix in its name, which was potentially confusing. Now, both properties are available in CatDat. The connection to distributivity has also been made more precise.
Finally, someone asked via the suggestion form to add concrete categories (or rather, concretizable categories, since for me and the nLab, "concrete" refers to extra structure, not a property). So this property has been added as well and decided for all categories in the database. In fact, only three categories in the database are not concretizable. This property had been on the list for quite a while, and I was hesitant to add it because I didn't see much value in it. But apparently, this was just my ignorance. After adding it, I learned about Isbell's condition for concretizability, which I find very interesting, applied it to the technical example mentioned at the beginning, and was thereby able to remove the proofs that no generating or cogenerating sets exist, since these now follow as corollaries of non-concretizability.
Having said this, I still do not know (cf. MSE) a single example of a concretizable and cocomplete category without equalizers, or, more or less equivalently, a practical example of a cocomplete category without equalizers.
Martin Brandenburg (Sep 10 2026 at 22:23):Release v1.20.0 adds several categories that are less common, but satisfy interesting property combinations that had not been witnessed before (e.g. f.g. projective modules over the ring of dual numbers, finite sets with even cardinality, posets without isolated points, and many more). In fact, the number of unwitnessed property combinations of categories of the form "p and not q" went down from 886 to 495.
There are now 112 categories in the database. In total, there are 195 categorical structures along with 23996 proofs of their properties (most of which are automated). Such statistics are now shown on the homepage, which has been redesigned completely.
Since categories in CatDat are not assumed to be locally small, it makes sense to drop this assumption also from preadditive and hence abelian categories. Following this change, several non-locally small abelian categories have been added, such as the functor category [On, Ab] ("long transfinite sequences of abelian groups"), which is an example of a Grothendieck abelian category that does not have a cogenerator. You might be familiar with the theorem that every Grothendieck abelian category has a cogenerator, but this is only true in the locally small case.
Even worse, there are Grothendieck abelian categories that are not complete (hence, not locally presentable), i.e. that do not have products. I have found an example for this combination which is very pathological and probably never comes up in practice, namely the category of vector spaces over a large field (such as surreal numbers) that have a small basis (details).
From all the new categories, all properties have been decided. Unfortunately (see here), some properties are still undecided for much more common categories, and I have started to think again about the difficult question if CMon has effective cocongruences (MO/511792).
Daniel Schepler has added total and cototal categories. There we also thought about allowing non-locally small categories, but decided against it because of the resulting technical issues and since MO/513986 did not receive any attention.
Martin Brandenburg (Sep 26 2026 at 19:52):Release v1.21.0 follows the same objective as the previous one; among other things, it adds 14 new categories that satisfy interesting property combinations. Just to name 5 of them:
All properties of the new categories have been decided (which has required a lot of work), with just one exception: I don't know if F(I)-Set is cototal.
The number of missing property combinations goes down from 495 to 321.
I don't think that every one of the remaining 321 combinations (see https://catdat.app/missing) needs to be witnessed by a category, since many of them are not very interesting. But some are: accessible but not well-copowered, Barr-exact but not (all) coequalizers, wide pullbacks but not cosifted limits, split abelian but not well-powered, quasitopos but not Barr-coexact, locally small but not concretizable (because hTop is still not added; and this category is only locally essentially small), locally presentable but not locally ℵ₁-presentable, Grothendieck topos but not finitary algebraic (we already have Sh(X) but need entries for special X to refute finitary algebraicness), finitely accessible but no sifted colimits, exact filtered colimits but no coequalizers, and many more ...
This PR implements a more consistent usage of essentially small collections, i.e. collections that are bijective to a set. This is a more precise version of what is often called a "small set" in the literature (and this wording is now removed from CatDat); it is confusing anyway since the literature often does not distinguish between elements of the universe U and elements of the next universe U+ that are isomorphic to elements in U – both are just called "small sets". But this is not correct, we cannot just ignore the difference (otherwise: what is the category Set?). CatDat now consistently distinguishes between sets (= small collections) and essentially small collections. This is akin to distinguishing between small categories and essentially small categories (namely, the discrete case). The page on foundations has been updated as well.
Martin Brandenburg (Sep 26 2026 at 20:29):I would also like to share that several of the recent non-trivial proofs in CatDat have been found with the help of Google Gemini (but, as always, I check everything in detail, restructure the proofs, fix mistakes, and put everything in my own words). I am using the Pro model, which is available for free for a couple of prompts per day. However, even though Gemini has found many interesting proofs, over the last few days it has been more frustrating than helpful, because it has made too many mistakes. In particular, it produced a lot of bullshit when trying to prove that the category of connected sequences of sets (mentioned above) does not have all ℵ₁-cofiltered limits. The same happened when trying to determine whether the category of F(I)-sets is cototal.
More and more, I get the impression that it is a waste of time to try to understand Gemini's output, since it eventually turns out to be wrong anyway. But I assume that (a) this is because the problems I want to solve have become quite difficult, (b) I do not use Deep Think (which, however, apparently requires the Ultra plan and thus costs €99.99 per month), or (c) perhaps I should not be using Gemini in the first place and should use a completely different tool instead. Is Claude better for (advanced) category theory?
David Michael Roberts (Sep 26 2026 at 22:23):@Martin Brandenburg does the example I give at that MO question about non-Grothendieck cocomplete toposes help at all? It's a way to get a large group action by an abelian group that is the "product of small groups", indexed by ORD. To my mind this might be easier to establish various properties. Also, it is definable without any essential use of universes (in ZF or presumably weaker), but of course it can be relativised.
And here's a property of elementary toposes that might be interesting: has a geometric morphism to Set. Obviously true for any Grothendieck topos, and for these toposes of large group actions, but not true for say the effective topos, but there are also cocomplete non-Grothendieck elementary toposes with a cocontinuous, lex functor from Set that has no right adjoint, for size reasons, coming from an ORD-indexed colimit of not-not sheaves on posets a la class forcing.
Not sure if you want to add it, but for the purposes of delineating the boundary of what's possible I personally found it interesting.
David Michael Roberts (Sep 26 2026 at 22:44):On a different note:
A collection is called countable if it admits a surjective map from the set of natural numbers
a surjective map from a subset of the naturals? Otherwise the empty set is not countable, but perhaps this is by design. In the classical setting you are in, subcountably-indexed = countable, but it's nice to not to have to treat the empty set as an additional special case, no?
Martin Brandenburg (Sep 27 2026 at 05:45):Thanks David, I saw your counterexample on MO but still need to check the details. The property "has a geometric morphism to Set" sounds indeed interesting, I have added it to the list of properties that I will add in the future.
And thanks a lot for spotting the mistake in the definition of a countable set! I will fix that now. The empty set should be countable, as every finite set actually.
Martin Brandenburg (Oct 06 2026 at 16:12):Release v1.22.0 adds various categories of graphs (in the form of sets equipped with certain binary relations, Example) and reduces the number of missing combinations from 321 (last release) to 249. For now, the goal of reducing that number is achieved.
Finally, the two remaining unknown properties of the category of commutative monoids have been decided: it is not cototal and does not have effective cocongruences. In fact, a finitary algebraic category is cototal if and only if it has a cogenerating collection! Kudos to Colin McQuillan and, well, to ChatGPT which found the proof, which yields a smooth transition to the next point.
I have also (finally?) started experimenting with Claude Code, and it is literally a game changer. In particular, I wrote a skill in this PR that is derived from the procedure how I add a new category, which includes deciding its properties and running several scripts, and of course, doing lots of mathematics. I then applied this skill to an empty file for the category of finitely generated groups. With the exception of 3 properties, all of its properties have been decided, and the proofs were already very good. I have then improved them even further.
Another very useful Claude skill that I have created is to proofread and also check the proofs in existing files. Lots of mistakes have been fixed already, but only a couple of files have been checked so far, and I am planning a global run.
Meanwhile, Claude also generated proofs for the 3 remaining properties of finitely generated groups (but this took longer), but I still need to check them, as they are not so easy. Claude also came up with a proof that the category of ω-sets, which Daniel Schepler is currently working on (PR), has no extremal generator. It is clearly much more powerful and makes less mistakes than Gemini (to be precise: Opus 5.5 versus Google Gemini 3.1 Pro), which I have been using before.
But also for the implementation of regular features, or writing up proofs from given sketches, Claude Code is much more convenient than typing out the code or text. I am pretty much late to the game, I know.
Even though all of this is very exciting, it also brings up very fundamental questions, such as "What is mathematics?" ... See also Is AI the End of Math As We Know It?
Morgan Rogers (he/him) (Oct 07 2026 at 08:49):To quote the student in the article you linked:
Goh is alarmed by how some have taken up AI without enough critical thought, and he feels pressured to use it so that he doesn’t get left behind. “I was just very depressed about that,” he said. “That doesn’t feel inspiring to me. … It didn’t have to be this way.”
I contacted you about figuring out one of the remaining properties of the category of commutative monoids; I worked on it for several days back in July and had hoped we could collaborate on turning the partial counterexample I had started constructing into a full one; your positive reaction in August suggested that this might happen, but you never recontacted me to follow up on it. Now I hear you're also discarding the efforts of other colleagues by feeding remaining problems that they were working on into AI systems.
Congrats on completing more of your database, I guess.