Zulip Chat Archive
Stream: maths
Topic: abelian categories
Johan Commelin (Jul 22 2019 at 06:11):
@Scott Morrison Now that we have monoidal cats, how far are we from abelian cats?
Scott Morrison (Jul 22 2019 at 07:18):
I think monoidal and abelian categories are just original directions to begin with. The roadmap towards abelian categories requires a bit more work on special shapes of limits, and the categorical API for kernels and cokernels.
Johan Commelin (Jul 22 2019 at 07:52):
I thought you wanted to use monoidal cats to define enriched cats and use those for abelian cats.
Scott Morrison (Jul 22 2019 at 08:00):
.... oh yeah. :-)
Scott Morrison (Jul 22 2019 at 08:01):
(Sorry, jetlag or something.)
Scott Morrison (Jul 22 2019 at 08:02):
I have a branch with some stuff on enriched categories. At least the beginning of the theory is pretty nice and straightforward.
Scott Morrison (Jul 22 2019 at 08:08):
You could write things like X \hom[V] Y to refer to the morphisms from X to Y, as an object of V. E.g. you could write something like X \hom[Ab] Y to obtain the (bundled) abelian group of chain maps between chain complexes X and Y.
Scott Morrison (Jul 22 2019 at 08:14):
oh... here's why you don't really need enriched categories first: a category with a zero object, binary biproducts, and all kernels and cokernels is automatically enriched in Ab!
Johan Commelin (Jul 22 2019 at 08:19):
I know... but that is a very mathematical statement.
Johan Commelin (Jul 22 2019 at 08:19):
We probably still want the enriched structure to be part of the definition (otherwise I fear diamonds will hit us).
Johan Commelin (Jul 22 2019 at 08:20):
And even if we don't, we still want to use the enriched structure. So we still need the theory of enriched cats.
Brendan Seamas Murphy (Dec 13 2019 at 00:54):
Has any progress been made on this? I'd be happy to help if there's an official roadmap somewhere
Brendan Seamas Murphy (Dec 13 2019 at 01:01):
I found https://github.com/leanprover-community/mathlib/issues/1063, but it seems like a big missing thing is Freyd-Mitchell (the embedding theorem). I'm interested in trying to do derived functors, but to construct the long exact sequence you need the snake lemma, which is a lot easier to prove if you have elements
Johan Commelin (Dec 13 2019 at 06:02):
Derived functors are a very nice target to motivate other development. But at the moment they seem a bit out of reach. But doing Freyd-Mitchell would of course be really helpful.
Johan Commelin (Dec 13 2019 at 06:03):
The problem with derived functors/categories is that there is so much stuff "up to isomorphism". And we currently don't have a good way of handling that in Lean.
Johan Commelin (Dec 13 2019 at 06:03):
My gut feeling says that it might be better to go for infty-categories directly.
Kevin Buzzard (Apr 20 2022 at 10:49):
Someone just pointed out to me this thesis https://github.com/tpannila/Masters_thesis/blob/master/An%20Introduction%20to%20Homological%20Algebra.pdf which I think pertains to this formalisation in UniMath: abelian categories five lemma short exact sequences
Last updated: Dec 20 2023 at 11:08 UTC