## 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.

Last updated: May 12 2021 at 08:14 UTC