Topic: Homological algebra
Markus Himmel (Mar 17 2020 at 17:25):
So with @Scott Morrison, @Kevin Buzzard and myself there are now at least three people working towards some form of homological algebra. Maybe now would be a nice moment to create a "project" on the mathlib GitHub repo for homological algebra, similar to what we already have for analysis? This could help to avoid duplicate efforts. For example, now that regular monos are coming soon, I am interested in strong monomorphisms and strong epi-mono factorizations, and it would be nice to know whether anyone else is working on this, so that the work isn't done twice.
Kevin Buzzard (Mar 17 2020 at 18:02):
I think this is a great idea. You know Scott has these mathlib branches which have been around for almost a year?! He wants to set up a general theory of enriched categories, and then define an additive category via being enriched over abelian groups, and then abelian categories on top of this. I think @Reid Barton and @Johan Commelin have also worked on homological algebra in the past, and @Floris van Doorn also knows a lot about homological algebra in Lean.
Bhavik Mehta (Mar 17 2020 at 23:16):
You may have seen already, but I've got regular epi-mono factorisations in locally cartesian closed categories with coequalizers, but other than that I don't imagine our topos theory project will have much overlap with what you're up to.
Markus Himmel (Mar 18 2020 at 08:35):
I have created the project at https://github.com/leanprover-community/mathlib/projects/2 and added some first cards. Please feel free to create issues and add them to the project. These issues could also be a good place to discuss design decisions before fully committing to some approach. For example, I would be very happy to hear your thoughts on #2178 and #2179.
Bas Spitters (Mar 18 2020 at 11:41):
There is also the homalg computer algebra package, based on GAP, that is programmed on a very categorical level:
They have an appreciation of type theory.
Last updated: May 09 2021 at 10:11 UTC