examples of (symmetric) monoidal categories

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4

https://leanprover-community.github.io/lean3

Apache License 2.0

1.67k stars 298 forks source link

examples of (symmetric) monoidal categories #1098

Closed kim-em closed 2 years ago

kim-em commented 5 years ago

We should provide some examples of monoidal categories. The absolutely fundamental ones are:

[x] Type (done in a branch)
[ ] AddCommGroup with tensor product
[x] Module (which needs to be defined first, per #1068) with tensor product
[x] the monoidal structure provided by the existence of products (draft)

jcommelin commented 4 years ago

Are these now all done?

kim-em commented 2 years ago

We don't quite have it on AddCommGroup, but we do have it for Module R, so I'm happy. We also have it for CommMon_ C, commutative monoid objects in any braided category.