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: community: our work

Topic: Martin Brandenburg


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

epis.webp

monos.webp

For now, I have added these diagrams on this page. They are not finished; for example, (effective) descent morphisms are currently missing.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip David Michael Roberts (Aug 16 2026 at 11:08):

Sorry I somehow missed the bit where you said you'd tried already!