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.
Patrick Nicodemus (Jul 24 2021 at 15:39):A lot of category theory is categorized by a lot of difficult and time consuming combinatorics. Recently I have been computing a lot of Kan extensions, adjoints, coends and so on between presheaf categories, and I am doing a lot of counting. Do any of you use software packages to help you explicitly describe a left adjoint, or a left Kan extension, or anything like that? I am thinking of something like SAGE or Macaulay2 or GAP but i have no idea whether these are useful for enriched category theory, monoidal category theory, or things like this. I have no experience with these tools.
Simon Burton (Jul 27 2021 at 13:29):What are you counting?
Patrick Nicodemus (Jul 27 2021 at 14:15):I guess in the cases where I can more explicitly describe what is to be counted I can rephrase the problem using standard combinatorics with the categorical language taken away. So for example, it's well known that the simplex category is the free monoidal category with distinguished monoid, aka the "Walking monoid." right now I'm working out simple cases of the other free monoidal categories. A general question we could ask is like, suppose I am interested in the free monoidal category (or free symmetric monoidal category) generated by objects m1,... mk together with these morphisms between them and their tensor products and modulo certain relations on morphisms. I can always describe this category in a very broad and vague way by generators and relations but like, for the simplex category we have a very short list of generators and relations and we can explicitly count the morphisms between objects in this category. To expand in the same direction I'd want to be able to do the same thing for categories enriched over pointed sets or Abelian groups, so that I could talk about relations on additive combinations of morphisms, i.e. talk about Lie algebras, derivations, things like that, and ask what the free category is generated by a Lie algebra in an Ab-enriched monoidal category, and explicitly count morphisms between objects.
One more example: if I have two small categories A and B, let's say indexed by the natural numbers, and a functor F : A -> B, and a presheaf P on A, there are standard formulas for how to compute the left/right Kan extension of P along F. In many cases we can very explicitly describe this in terms of P. I should be able to program a computer to compute this Kan extension much the same way I do it in practice: I figure out some generators and relations presentation of the morphisms in the categories and then the left Kan extension is given by all formal pairs (f,x) with f : c -> d and x\in P(d), modded out by certain equivalence relations. I want to describe what this set looks like in a way that isn't just the naive/abstract presentation.
Simon Burton (Jul 27 2021 at 15:27):Woah, this is super interesting to me.
Simon Burton (Jul 27 2021 at 15:29):I don't think macaulay2 or GAP can cope with anything like this, but sage is always growing so it might be worth digging there... Where are you on the like-hate spectrum with regards programming ?
Patrick Nicodemus (Jul 27 2021 at 15:53):I don't currently use programming in my work and so my skills are very rusty. But I'd be happy to pick it back up.
Timothy Porter (Jul 27 2021 at 19:34):Perhaps you might be interested in Anne Heyworth's thesis from Bangor many years ago (we were way ahead of our time!) Some idea of what it contains can be gleaned from Ronald Brown, Anne Heyworth:
Using Rewriting Systems to Compute Left Kan Extensions and Induced Actions of Categories. J. Symb. Comput. 29(1): 5-31 (2000)
One of the points is that sometimes rewriting theory is well adapted for calculations. Another point in the thesis is the use of Grobner Bases in such calculations. The thesis is at https://arxiv.org/abs/math/9812097.
Evan Patterson (Jul 28 2021 at 05:41):Thanks for sharing these interesting problems. I am also interested in computational category theory. In Catlab, we have a fairly mature implementation of presheaves over finitely presented categories. For example, we can compute limits and colimits in presheaf categories and we can enumerate the homomorphisms between two presheaves (with the caveat that homomorphism finding is generally NP-hard).
So far we have been more focused on combinatorial data structures and algorithms than symbolic computer algebra, and we certainly can't do all of the things you described. However, I'd like to make some forays in this direction. For instance, besides its theoretical interest, computing left and right Kan extensions in presheaf categories has very practical applications (Spivak's "functorial data migration"). There is a small literature on computing Kan extensions, but I haven't yet delved into it. I'd be willing to try coding something up as long as it doesn't seem too hard and complicated.
Evan Patterson (Jul 28 2021 at 05:43):Timothy Porter said:
Perhaps you might be interested in Anne Heyworth's thesis from Bangor many years ago (we were way ahead of our time!)
Wow, I'm surprised I hadn't seen this thesis. It looks super cool. Thanks!
Timothy Porter (Jul 28 2021 at 11:53):Checkout Anne's other papers on rewriting. etc. https://www.researchgate.net/profile/Anne-Heyworth
The papers are now about 15 years old, so some of the ideas may have been given other names since.
Other people to look at as being interested in the rewriting aspect are [Philippe Malbos (http://math.univ-lyon1.fr/homes-www/malbos/) and Yves Guiraud) (https://webusers.imj-prg.fr/~yves.guiraud/). There are several other people in Lyon or Paris who might be worth following.
It would be great to see some interaction between the rewriting / Grobner basis stuff and recent advances in ACT.
Amar Hadzihasanovic (Jul 28 2021 at 12:20):I was not aware of Anne's work either! Thanks for advertising it!
Cody Roux (Jul 28 2021 at 18:30):Paging dr @Philip Zucker ...
Philip Zucker (Jul 28 2021 at 20:49):This is a really interesting thread to me. I've played with trying to encode categorical problems to some of the systems out there, in particular SMT solvers and Automated Theorem Provers with very mixed success and failure https://www.philipzucker.com/theorem-proving-for-catlab-2-lets-try-z3-this-time-nope/ https://www.philipzucker.com/category-theory-in-the-e-automated-theorem-prover/ . I don't have a system ready to use. I do think it sounds interesting and doable to take truly finite category theory problems and encode them to SAT, but such a problem is more the exception than the rule https://www.philipzucker.com/z3-and-the-word-problem/ . I'm currently on a kick of trying to use egraphs to encode category theory. It gives you a notion of equality and quantification to play with that seems useful https://www.philipzucker.com/rust-category/ https://www.philipzucker.com/egglog-checkpoint/ None of these really would ever have the flavor of GAP or Macaulay, which are big systems.
Timothy Porter (Jul 29 2021 at 17:45):Evan, I mentioned your interest to Ronnie Brown and he said if you would like to discuss Anne's work more you are welcome to contact him on ronnie.probrown@btinterne5t.com. He finds the type here on Zulip difficult to read so cannot reply here. (but he did! see below, but change the obvious typo in the address of the website.)
Ronald Brown (Jul 29 2021 at 17:50):Please send message to ronnie.profbrown@btinternet.co since I have eysight problems. My web site is www.gropoids.org,.uk .I was Anne's supervisor and there is more to say.
Evan Patterson (Jul 30 2021 at 01:47):Tim and Ronnie, thank you both! My own email address is evan@epatters.org. I'll send an email once I've had time to digest more of the thesis.
Patrick Nicodemus (Nov 03 2021 at 21:49):https://www.cs.cornell.edu/~kozen/Papers/06ijcar-categories.pdf
Patrick Nicodemus (Nov 03 2021 at 21:49):cool paper!
Patrick Nicodemus (Nov 03 2021 at 21:51):The authors give a formal system and some tactics automatically proving theorems in category theory. They show that these tactics can be used to automatically prove that the category Cat is cartesian closed. Neat!
Patrick Nicodemus (Nov 03 2021 at 21:51):I don't know how "automated" it is exactly but the full proof looks to be around 3,000 lines and i doubt they wrote the bulk of that by hand.
Daniel Teixeira (Nov 04 2021 at 15:41):neat! that paper isn't even new, I wonder about what other research in a similar vein happened in between
Spencer Breiner (Nov 05 2021 at 13:28):They note that a judicious choice of lemmas reduces the length by a factor of ten, down from ~30,000 lines.