additive functors

Stream: Is there code for X?

[Adam Topaz]

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

[Bhavik Mehta]

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

[Adam Topaz]

Ah I see.

[Scott Morrison]

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.

[Adam Topaz]

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

[Scott Morrison]

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

[Scott Morrison]

but yes

[Scott Morrison]

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