issue #2176: Define preadditive categories

Stream: triage

[Random Issue Bot]

Today I chose issue 2176 for discussion!

Define preadditive categories
Created by @Markus Himmel (@TwoFX) on 2020-03-18
Labels: feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

Preadditive categories are defined in category_theory.preadditive.default so I'm guessing we can close this one.

[Kevin Buzzard]

There is also this project: https://github.com/leanprover-community/mathlib/projects/2#card-34755971 which we might also be able to update.

[Markus Himmel]

My understanding is that the current definition is just a "temporary" one while we wait for enriched categories

[Markus Himmel]

I'm not sure how much progress there has been towards enriched categories. There is branch#enriched_reprise which had some recent commits but I don't know what it does.

[Kevin Buzzard]

Maybe someone should update the issue with these comments?

[Bhavik Mehta]

@Scott Morrison would be most helpful here, but my understanding from the last time I asked him was that there's a bunch of tricky questions to ask about how to go about setting up definitions in order to make them useful for concrete applications; and perhaps the right approach for the moment is to consider concrete enriched categories, ie ones where the hom-sets are sets with some extra structure (eg additive groups) rather than replacing hom-sets with objects from any monoidal category

[Bhavik Mehta]

Quoting from him so as to save him some typing:
"We could just enrich over an arbitrary monoidal category V (not necessarily concrete), and then do base change along any lax monoidal functor, and then set up the equivance between Type-enriched categories and ordinary categories. This is certainly the most "principled" approach. But I don't think it helps anyone who just wants to be able to multiply their morphisms by scalars (and know their functors commute with scalar multiplication, etc, etc"

[Scott Morrison]

branch#enriched_reprise seemed like a promising start on V-enriched categories in the special case where the V is a concrete category and moreover is built using src#bundled_hom. While this works great for V = Group or V = AddCommGroup, it wouldn't work for V = Module R.

[Scott Morrison]

I'm not sure it's useful to have a setup where there is a different incantation to talk about an AddCommGroup enriched category and a Module R enriched category. :-(

[Scott Morrison]

In any case I think there's going to be a certain amount of boilerplate for each different value of V(e.g. we can't set up instances which a polymorphic in the typeclass, so at the very least we're going to have to say for each separate V that the hom types actually carry the class).

[Scott Morrison]

Given that, it may actually just be fine to go the "principled" route.

[Scott Morrison]

I think this would consist of a class enriched_category V C, which is actually disconnected entirely from category, which provides an term of V between each X Y : C, even when V is not concrete. We'd further have change-of-enrichment along a lax monoidal functor V ⥤ W. Finally there would be a typeclass enriched_over V C, which would be a mixin for category C, which would contain the data of a enriched_category V C, along with the equivalences that show that when you transport that one to Type you get the original category C.

[Scott Morrison]

(When I say "you get the original category" here, you have to do it pretty gorily: the transported thing will be an enriched_category (Type u) C, and the original thing is a category C, and these are not the same gadget, just equiv.)

[Scott Morrison]

The problem with going this route is that you have to build a bunch of theory about enriched_category, before you ever get to find out if the design is actually usable in concrete cases like V = Top or V = Module R...

[Bhavik Mehta]

Scott Morrison said:

The problem with going this route is that you have to build a bunch of theory about enriched_category, before you ever get to find out if the design is actually usable in concrete cases like V = Top or V = Module R...

This doesn't sound like a problem to someone like me who cares more about the theory than the concrete examples :D