Homological algebra

Stream: maths

[Markus Himmel]

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]

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]

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]

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]

There is also the homalg computer algebra package, based on GAP, that is programmed on a very categorical level:
https://homalg-project.github.io/
They have an appreciation of type theory.