Free strict n-categories

Stream: Is there code for X?

[Tim Campion]

Hi, I'm new here, and not sure if this is the right place for the following question, but here goes.

I'm a category theorist who's wanted to learn more about Lean for awhile now, and I have an idea for a project which would push me to learn some Lean. The project would be to formalize some basic results about strict n-categories, and specifically about various "presentations" of strict n-categories.

There are several formalisms in the literature for doing this. The most general one is the formalism of "computads", or "polygraphs" as the French call them. In the n-category presented by a computad, a k-cell is represented as an equivalence class of words in a generating set of cells. Then there are a bunch of more restricted formalisms, which generally represent a k-cell as a particular kind of subset of the generating cells -- they're more restricted because in general subsets are not expressive enough. An overview of some of these formalisms (and long-overdue comparison between them) is found in Simon Forest's thesis.

This subject already has an interesting history vis à vis formalization. One of the first of the more "restricted" formalisms was introduced by Street, his Parity Complexes. An error was found in the main theorem (asserting the correctness of the construction of the free n-category using subsets of generators) , and a corrigendum published. I suspect this messy state of affairs partly motivated Buckley to formalize the paper in Coq, but he was unable to formalize the main theorem. Finally, a counterexample to the "corrected" version of the main theorem was given by Forest, along with a new proof of the main theorem under additional hypotheses.

So I have a few reasons to be interested in formalizing the freeness theorem for parity complexes or some variant:

1. Some of the history of this subject has already been driven by formalization, so it would be only natural to continue the formalization thread of the story.

2. Personally, I tend to find Forest's treatment of the freeness theorem to be much more detailed than Street's, and the comprehensiveness of his work convinces me that it is probably (finally!) actually correct. Nevertheless, formalizing this stuff would erase some lingering reasonable doubts.

3. Part of what makes these structures error-prone to work with is that there's a fair bit of fiddly combinatorics which goes into using them. My naive sense is that this "fiddliness" is the sort of thing which could be ameliorated by having formalized libraries to work with.

4. When some formalization has already been done in Coq, what is the best way to leverage such prior work in a Lean formalization project?

5. (for me) it would be an excuse to learn some Lean!

There are a bunch of obvious first questions to ask, like:

• Has this already been done? (my guess is: no!)

• How much of a library for n-categories exists? (my guess is: not much for n > 1!)

• One of the alternatives to Street's parity complexes is Steiner's augmented directed complexes, which are based on the linear algebra of free Z-modules rather than manipulations of subsets of a given set. Given a choice between working with such linear algebra in Lean versus manipulation of subsets in Lean, what would be some of the pros / cons to either choice?

• I'm guessing such a project might take 100 hours to write. Should I multiply my guess by 10 ? 100 ? 1000?

[Adam Topaz]

Welcome @Tim Campion ! To answer (some of) your questions: We don't have anything about n-categories for $n > 2$, but we recently got bicategories thanks to the work of @Yuma Mizuno . We also have some code for simplicial sets, and at least a few folks (myself included) who have contemplated defining higher categories via the simplicial route.

[Johan Commelin]

@Tim Campion Great to see you here!

When some formalization has already been done in Coq, what is the best way to leverage such prior work in a Lean formalization project?

Unfortunately, at the moment there is very little possible when it comes to automatically importing or porting work from one proof assistant to another.

I'm guessing such a project might take 100 hours to write. Should I multiply my guess by 10 ? 100 ? 1000?

100 hours is ≤ 2.5 full-time weeks (depending on the length of a full-time week :stuck_out_tongue_wink:). If your time estimate includes getting familiar with Lean, I think you should probably multiply it by a factor between 10 and 100.

Given a choice between working with such linear algebra in Lean versus manipulation of subsets in Lean, what would be some of the pros / cons to either choice?

Hard to say. (Especially since all my experience with categories deals with the n = 1 case. The number of hours spent with n =2 or n = ∞ can be counted on the fingers of very few hands.)

But there is a general principle that seems to hold when it comes to formalisation, namely that the more abstract (categorical?) and "free" approach to a subject is usually the smoothest way forward. So I imagine that the linear algebra of free ℤ-modules might score slightly better in that respect.

[Kevin Buzzard]

I think that it's very difficult to make time estimates. In 2017 after 100 hours from knowing 0 about lean and only having #tpil and this chat as a guide, I was probably writing gigantic proofs of the irrationality of sqrt(3) and feeling very proud of myself. However it's worth pointing out that (a) now we have much better teaching material for mathematicians and (b) I was also having a huge amount of fun.

[Kevin Buzzard]

I had also realised that learning lean by leaping into a project and then spamming this chat with questions was an extremely effective way to do it. That's why I started on schemes the moment I'd understood the basics. The community gave me the support I needed.

[Johan Commelin]

It also matters a lot whether you want a time estimate for writing the definitions of n-categories or formalising the proof of the freeness theorem that you mentioned.