Zulip Chat Archive

Stream: triage

Topic: issue #2176: Define preadditive categories


view this post on Zulip Random Issue Bot (Apr 11 2021 at 14:23):

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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 11 2021 at 19:12):

Maybe someone should update the issue with these comments?

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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. :-(

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Apr 11 2021 at 23:20):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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...

view this post on Zulip 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