## Stream: triage

### Topic: issue #2176: Define preadditive categories

#### Random Issue Bot (Apr 11 2021 at 14:23):

Today I chose issue 2176 for discussion!

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 (Apr 11 2021 at 18:05):

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

#### Kevin Buzzard (Apr 11 2021 at 18:06):

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 (Apr 11 2021 at 18:58):

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

#### Markus Himmel (Apr 11 2021 at 19:02):

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 (Apr 11 2021 at 19:12):

Maybe someone should update the issue with these comments?

#### Bhavik Mehta (Apr 11 2021 at 19:31):

@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 (Apr 11 2021 at 19:32):

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 (Apr 11 2021 at 23:17):

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 (Apr 11 2021 at 23:17):

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 (Apr 11 2021 at 23:19):

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 (Apr 11 2021 at 23:20):

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

#### Scott Morrison (Apr 11 2021 at 23:22):

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 (Apr 11 2021 at 23:24):

(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 (Apr 11 2021 at 23:25):

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 (Apr 12 2021 at 03:01):

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

Last updated: May 09 2021 at 16:20 UTC