AddCommMonoid enriched categories

Stream: Is there code for X?

[Bernhard Reinke]

Is there already code for categories enriched over additive commutative monoids? So like preadditive categories, just without the inverses for addition? Similarly, for semirings, I think at the moment a linear category over a semi-ring is assumed to be preadditive. Is there a way to get rid off the assumption of the existence of additive inverses?

[Kim Morrison]

No, this is not done. You could perhaps used the generic EnrichedCategory formalism, but it will be a battle every step of the way.

[Kim Morrison]

What is your application?

[Bernhard Reinke]

I think it makes sense to define the category semi-ring of a category enriched over additive commutative monoids. I have a construction for the category ring of a preadditive category, but I don't think I really need negatives to prove associativity. At the moment I want to understand what the correct generality for my PR #22823 surrounding the associator of a ring should be.

[Jakob von Raumer]

@Kim Morrison Do you know if anyone has started to connect Preadditive to that formalism?

[Kim Morrison]

@Jakob von Raumer, I don't think so. I tried doing so during initial attempts at setting up enriched categories, but it never survived through to what's in Mathlib.

[Jakob von Raumer]

There's not even the monoidal structure on AddCommGrp or am I just not finding it?

[Jakob von Raumer]

Ah, we have it through modules

[Jakob von Raumer]

Kim Morrison said:

Jakob von Raumer, I don't think so. I tried doing so during initial attempts at setting up enriched categories, but it never survived through to what's in Mathlib.

FWIW I started another attempt at #23826, finished one direction of what ideally should become an equivalence of the bicategories