Zulip Chat Archive

Stream: maths

Topic: abelian categories


view this post on Zulip Johan Commelin (Jul 22 2019 at 06:11):

@Scott Morrison Now that we have monoidal cats, how far are we from abelian cats?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 22 2019 at 08:00):

.... oh yeah. :-)

view this post on Zulip Scott Morrison (Jul 22 2019 at 08:01):

(Sorry, jetlag or something.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jul 22 2019 at 08:19):

I know... but that is a very mathematical statement.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 13 2019 at 06:03):

My gut feeling says that it might be better to go for infty-categories directly.


Last updated: May 12 2021 at 08:14 UTC