Zulip Chat Archive

Stream: Is there code for X?

Topic: additive functors


view this post on Zulip Adam Topaz (Feb 15 2021 at 15:33):

Does the abelian categories part of mathlib have something about additive functors? I can't even find a definition.

view this post on Zulip Bhavik Mehta (Feb 15 2021 at 18:52):

None that I know of - @Scott Morrison would know better than I though. If I remember correctly, the idea was to define enriched categories and functors of those first, and deduce additive functors from these? Also I think there was a student of @Kevin Buzzard, who was interested in this too

view this post on Zulip Adam Topaz (Feb 15 2021 at 18:52):

Ah I see.

view this post on Zulip Scott Morrison (Feb 16 2021 at 00:33):

Exactly right --- my dissatisfaction with all my attempts at enriched categories has held up other things. Perfect being the enemy of best, I think we should just do additive functors.

view this post on Zulip Adam Topaz (Feb 16 2021 at 01:33):

@Scott Morrison we're you thinking of defining additive categories (preabelian?) categories as categories enriched over Ab?

view this post on Zulip Scott Morrison (Feb 16 2021 at 02:00):

preadditive I guess is the term for enriched-over-Ab

view this post on Zulip Scott Morrison (Feb 16 2021 at 02:00):

but yes

view this post on Zulip Scott Morrison (Feb 16 2021 at 02:01):

I seem to have forgotten where I got up to with enriched categories. It was pretty unsatisfactory.


Last updated: May 16 2021 at 05:21 UTC