to_additive on MonoidalCategory

Stream: mathlib4

[Jad Ghalayini]

I'm trying to get my PhD thesis ported from my custom discretion library to mathlib, and in the process of doing so, need to introduce an additive version of monoidal categories to have an idiomatic way to equip a category with a chosen cocartesian structure. This could also open the door to formalization of general rig categories, someday.

In my PR #30150 (https://github.com/leanprover-community/mathlib4/pull/30150) I introduce AddMonoidalCategory as the to_additive version of MonoidalCategory, and tag most of the definitions and theorems in CategoryTheory/Monoidal/Category with to_additive. To avoid breaking changes, I also need to make some slight edits to CategoryTheory/Monoidal/Discrete.

@Yaël Dillies told me to start a discussion to acquire consensus on new names and notations. In particular:

• The to_additive version of MonoidalCategory is AddMonoidalCategory
• The to_additive version of tensor is just add. I didn't want to use something like "direct sum" since that's not necessarily what this is.
• We use the notation ⊕ₒ for adding objects and ⊕ₘ for adding morphisms. We don't use a bare ⊕ to avoid confusion with the sum of types
• We use the notation 𝟘_ C for the unit of ⊕ₒ and α⁺, λ⁺, ρ⁺ for the additive versions of the associator and unitors

I'd also like to take the opportunity to solicit community feedback on some other proposed syntax/naming for future PRs:

• AddBraidedCategory for the additive version of BraidedCategory
• β⁺ for the additive version of the braiding morphism
• AddSymmetricCategory for the additive version of SymmetricCategory
• CocartesianMonoidalCategory for when ⊕ₒ is a coproduct on objects
• AddFreeMonoidalCategory for the additive version of FreeMonoidalCategory; to port coherence we need a proper AddMonoidalCategory instance for Discrete and an AddMonoid instance for AddNormalMonoidalObject, which we should probably get along to making.
• ⋉ and ⋊ for the left and right ordered tensor products in a PremonoidalCategory; I wouldn't bother with additive versions since while we want an AddPremonoidalCategory to simplify working with to_additive having one which is not also an AddMonoidalCategory is somewhat unidiomatic
• A Central f typeclass for when f ⋉ g = f ⋊ g and g ⋉ f = g ⋊ f for all g

[Sina Hazratpour]

I think I prefer CocartesianMonoidalCategory to CocartesianAddMonoidalCategory. Also, would there be a real confusion if we used ⊕? I mean the sum types do give the cocartesian monoidal structure on the category of types. What goes wrong if we overload this notation?

[Sina Hazratpour]

(Incidentally, for some project, I worked with internal semirings, so added the files AddMon_.lean and AddCommMon_.lean to my project, and once your PR is there, I'd be happy to add these to mathlib.)

[Jad Ghalayini]

Hello! Any updates on where this is at?

[William Sørensen]

I would also find this very useful for formalising the Cambridge category theory course

[Sina Hazratpour]

Jad Ghalayini said:

Hello! Any updates on where this is at?

currently, it's a private repo, but intend to release it soon; happy to coordinate with you to PR part of the code (AddMon_.lean, AddCommMon_.lean, SemiringObj, etc) to mathlib if you want.