Learning Mathlib's category theory

Stream: Infinity-Cosmos

[Thomas Murrills]

I thought it might be useful to have a catch-all topic for learning Mathlib's implementation of category theory (assuming basic familiarity with 1-, 2-category theory mathematically) for people who might like to contribute to this project, but who don't have the library familiarity (like myself).

I'd encourage anyone else who's learning Mathlib's take on categories to ask questions here as well, and to share things they found unexpected or counterintuitive! (That is, please don't consider this "my" topic.) :)

For a point to start from, I'm currently working through these exercises which were linked in #Lean Together 2025 > Emily Riehl: The infty-cosmos project.

[Jack McKoen]

Good idea! The category theory library can be tough to get used to :) I've been thinking for a while that something like the natural number game could be useful for this (but I've been too busy to work on something like it)

[Thomas Murrills]

By the way, re: those exercises, I'm noticing that there have been some adjustments to the RingCat API in the time since Exercise 2 was written; some imports are renamed, and the data of the category is structured a bit differently (arrows are wrapped in a one-field structure, for instance)! Also, some hints are in fact misleading (e.g. "use cancel_mono"): it seems that the warning in the README ought to be heeded :)

Note: Others could have ported these exercises. Right now some of the hints no longer exist, others might be misleading. I have only solved half of the exercises so can't guarantee that I ported them all correctly.

[Kevin Buzzard]

Please feel free to update! I think that exercises are the best way to learn, my imperial undergrad course is basically just all exercises (covering a bunch of mathlib but notel category theory) and I update it once a year (in fact it's now Bhavik's course and hopefully he updated it this year) but the category theory exercises are just a random thing which gets occasionally noticed. Maybe @Bhavik Mehta you want to add them to the Imperial course repo?

[Bhavik Mehta]

I haven't added them yet, but I'm hoping to soon!

[Thomas Murrills]

Kevin Buzzard said:

Please feel free to update!

Happy to! :) Let me know where the best place to PR is, ultimately; some updates (like misleading hints) would make sense for the CopenhagenMasterclass2023 repo, but some API-based updates would only make sense on current Mathlib (which hasn’t propagated to that course). (I deliberately tried to solve these exercises on current Mathlib to make sure I wasn’t learning outdated API. :) )

[Thomas Murrills]

And/or I can help prepare them for the Imperial course, if that’s desired. :)

[Kevin Buzzard]

Bhavik did you release an FM25 course? If so then Thomas could just PR them as section 23 or whatever we're up to!

[Bhavik Mehta]

Yup, it's here: https://github.com/b-mehta/formalising-mathematics-notes

[Thomas Murrills]

I'm compiling a little dictionary between category theoretic concepts and Mathlib's notation/implementation/design choices. Would this table be welcome in some communal location, e.g. the Mathlib manual or the wiki? (Does something like this exist already?)

(Also, I'm back from some time away now, so I'll hopefully get around to PRing those exercises soon. :) )

[Markus Himmel]

There is https://leanprover-community.github.io/theories/category_theory.html but it's very incomplete and I would be very happy to review and merge PRs that expand this page.

[Sina Hazratpour 𓃵]

@Markus Himmel I think it would be extremely helpful to have more notation/implementation/design choices on the page you mentioned! I'll PR bunch of things I recorded locally for my own use. I intended to put them in a blog post on website, but i think the page you shared is a much better place.

[Thomas Murrills]

Markus Himmel said:

There is https://leanprover-community.github.io/theories/category_theory.html but it's very incomplete and I would be very happy to review and merge PRs that expand this page.

Ok, great! :)

I'm trying out a couple different ways of organizing the information, which you can see in (only) the Categories section here.

This would split each section into Design and Notation subsections; the design subsection would start by introducing the basic way the mathematical concept is represented in Mathlib, then elaborate on implementation details.

The Notation subsection could either be a bulleted list or a small table; I've tried out a bulleted list, a table, and a condensed table in that branch.

I'm also wondering if it would be useful to have a single table somewhere on that page that collects all the notation, and just the notation. Maybe it would make sense to stick to a textual bulleted list in each individual Notation subsection in this case!

(My first approach was to have a single table that collected everything, but introducing the design in that table ultimately seemed unwieldy and not reader-friendly.)

@Sina Hazratpour 𓃵, please feel free to propose organizing it a different way, given your own notes! I'm just experimenting here. :)

[Sina Hazratpour 𓃵]

Thanks for sharing your thoughts. I like the idea of a table that collects all the notations.
I also don't know how long we think this page would/should be, so for instance thing like why we implement concept X in this way and not the standard way in the Elephant or nlab or whatever canonical reference. My notes are basically a personal mnemonic device for useful tactics and tricks in category theory, but I don't know if or to what extent they are prescriptive. And ofc things get outdated/updated sometimes (e.g. tidy is now subsumed by aesop?).

[Thomas Murrills]

Sina Hazratpour 𓃵 said:

I also don't know how long we think this page would/should be, so for instance thing like why we implement concept X in this way and not the standard way in the Elephant or nlab or whatever canonical reference.

Hmm, good point—I think a worthy mission for this page should be to prioritize "initiating the uninitiated", i.e. explaining the basics of how category theory is set up in Mathlib and how to work with it.

Maybe detailed explanations and justifications of the implementation details (e.g. "we do it this way, not that way, because of this technical reason...") should be either (1) in a toggleable "Implementation details" subsection—accessible for the curious, but doesn't take up space or scare off new users or (2) only present in the cource code documentation, and removed from the page entirely.

I'd favor (1) (or some other way of making this information accessible here!), but I could understand (2).

Sina Hazratpour 𓃵 said:

My notes are basically a personal mnemonic device for useful tactics and tricks in category theory, but I don't know if or to what extent they are prescriptive. And ofc things get outdated/updated sometimes (e.g. tidy is now subsumed by aesop?).

I think it would be useful to have another section called something like "How to work with category theory" or "Proving theorems" that catalogued this sort of information! That is: there's understanding how Mathlib's category theory is set up conceptually and how to read statements (in Design and Notation), then there's understanding how to interact with the library. Both are important, and decouple nicely!

[Sina Hazratpour 𓃵]

Between (1) and (2) you suggested above, i also think (1) is more feasible.