Currently, CatDat supports three types of categorical structures: categories, functors, morphisms. This issue is about adding symmetric monoidal categories. It is a follow-up of #4. See #290 for a similar issue.
Every symmetric monoidal category should have an underlying category which is recorded in the database.
Some examples:
- $(Set,\times,1)$
- $(Top,\times,1)$
- $(Set,\sqcup,0)$
- $(Cat,\times,1)$
- $(Set_*,\wedge,\{0,1\})$
- $(Ab,\otimes,Z)$
- $(Ab_{fg},\otimes,Z)$
-
$(Mod_R,\otimes_R,R)$ (where $R$ is a commutative ring)
-
$(grMod_R, \otimes_R,R)$ with the symmetry $\sigma(a \otimes b) = b \otimes a$
-
$(grMod_R, \otimes_R,R)$ with the symmetry $\sigma(a \otimes b) = (-1)^{|a| \cdot |b|} \cdot b \otimes a$
- $(Sh(X,Ab),\otimes,\underline{\mathbb{Z}})$
- $(N,+)$
- $([0,1],+)$
- $(Ban,\otimes_p,C)$
Some properties:
- cartesian
- cocartesian
- closed
- strict
- distributive (i.e. the underlying category has coproducts and $\otimes$ preserves coproducts in each variable)
- cocomplete (i.e. the underlying category is cocomplete and $\otimes$ preserves colimits in each variable)
(!) Properties that only refer to the underlying category are not added to the database. There is no need.
The mentioned properties should be decided for the mentioned symmetric monoidal categories.
If $(C,\otimes,1)$ is a symmetric monoidal category, then $(C^{op},\otimes,1)$ is a symmetric monoidal category; dual properties refer to this kind of dualization. The other kind of dualization, using $\otimes^{op}$, only becomes relevant for monoidal categories, which are not the subject here.
Technical detail: for URLs, the type should be with underscores symmetric_monoidal_category, but for text, it should be with spaces symmetric monoidal category. Thus, one needs to differentiate between these two use cases (which was not necessary before). Maybe this can be a separate PR before adding symmetric monoidal categories.
As a follow-up, symmetric monoidal functors can be added as well.
Currently, CatDat supports three types of categorical structures: categories, functors, morphisms. This issue is about adding symmetric monoidal categories. It is a follow-up of #4. See #290 for a similar issue.
Every symmetric monoidal category should have an underlying category which is recorded in the database.
Some examples:
Some properties:
(!) Properties that only refer to the underlying category are not added to the database. There is no need.
The mentioned properties should be decided for the mentioned symmetric monoidal categories.
If$(C,\otimes,1)$ is a symmetric monoidal category, then $(C^{op},\otimes,1)$ is a symmetric monoidal category; dual properties refer to this kind of dualization. The other kind of dualization, using $\otimes^{op}$ , only becomes relevant for monoidal categories, which are not the subject here.
Technical detail: for URLs, the type should be with underscores
symmetric_monoidal_category, but for text, it should be with spacessymmetric monoidal category. Thus, one needs to differentiate between these two use cases (which was not necessary before). Maybe this can be a separate PR before adding symmetric monoidal categories.As a follow-up, symmetric monoidal functors can be added as well.