Add symmetric monoidal categories

.cspell.json

@@ -72,6 +72,7 @@
 		"codiagonal",
 		"codirected",
 		"codistributive",
+		"codistributivity",
 		"codomain",
 		"codomains",
 		"coequalized",
@@ -145,6 +146,7 @@
 		"Duskin",
 		"Easton",
 		"Eilenberg",
+		"endofunctor",
 		"endofunctors",
 		"Engelking",
 		"epimorphic",
@@ -179,6 +181,7 @@
 		"Haus",
 		"hausdorff",
 		"Hertweck",
+		"Heunen",
 		"Heyting",
 		"homotopic",
 		"homotopy",
@@ -226,6 +229,7 @@
 		"monic",
 		"monoid",
 		"monoidal",
+		"monoidally",
 		"monoids",
 		"monomorphism",
 		"monomorphisms",
@@ -321,11 +325,13 @@
 		"uncountably",
 		"unital",
 		"unitalization",
+		"unitor",
 		"Universalis",
 		"Universitext",
 		"Urysohn",
 		"vercel",
 		"Verlag",
+		"Vicari",
 		"Vincenzo",
 		"Vite",
 		"Wedderburn",

DATABASE.md

@@ -10,7 +10,7 @@ The local copy of the database is located at `/database/catdat.db`. It contains
 - `properties`
 - `implications`
 
-The `structures` table stores data that is common to all types of categorical structures. Three types are currently supported: categories, functors, and morphisms. They are stored in the following table:
+The `structures` table stores data that is common to all types of categorical structures. Three types are currently supported: categories, functors, morphisms, and symmetric monoidal categories. They are stored in the following table:
 
 - `structure_types`
 
@@ -19,6 +19,7 @@ Structure-specific data is stored in additional tables, such as:
 - `categories`
 - `functors`
 - `morphisms`
+- `symmetric_monoidal_categories`
 
 Properties (whether satisfied or not) are associated with categorical structures via the following table:
 

README.md

@@ -7,13 +7,13 @@
 
 ## [**https://catdat.app**](https://catdat.app)
 
-_CatDat_ provides a growing collection of categorical structures such as categories, functors, and morphisms, each with detailed descriptions and properties. Built by and for those who love [category theory](https://en.wikipedia.org/wiki/Category_theory).
+_CatDat_ provides a growing collection of categorical structures such as categories, functors, morphisms, and symmetric monoidal categories, each with detailed descriptions and properties. Built by and for those who love [category theory](https://en.wikipedia.org/wiki/Category_theory).
 
 [Watch the YouTube video](https://youtu.be/dQXbPxk__qA)
 
 ## Features
 
-- **Types of Categorical Structures**: Supports categories, functors, and morphisms.
+- **Types of Categorical Structures**: Supports categories, functors, morphisms, and symmetric monoidal categories.
 - **Structure Detail Pages**: Each categorical structure has a dedicated page with its definition, satisfied and unsatisfied properties, and related structures.
 - **Property Detail Pages**: Explore the definition of a property and view categorical structures that satisfy it and those that don't.
 - **Proofs and References**: Each property and implication includes a proof or reference, forming a data-driven knowledge base for category theory.

content/dual-properties.md

@@ -28,3 +28,11 @@ Given a property $P$ of morphisms, its dual property $P^{\op}$ is defined as fol
 For example, the property [monomorphism](/morphism-property/monomorphism) is dual to [epimorphism](/morphism-property/epimorphism) since $f$ is an epimorphism if and only if $f^{\op}$ is a monomorphism.
 
 Notice that $(P^{\op})^{\op} = P$, and that $f$ satisfies $P$ if and only if $f^{\op}$ satisfies $P^{\op}$.
+
+### Symmetric Monoidal Categories
+
+The dual of a symmetric monoidal category $(\C,\otimes,1)$ is defined by $(\C^{\op},\otimes,1)$ (and the obvious coherence isomorphisms). Given a property $P$ of symmetric monoidal categories, its dual property $P^{\op}$ is defined as follows: a symmetric monoidal category satisfies $P^{\op}$ if and only if its dual satisfies $P$.
+
+For example, the properties [closed](/symmetric_monoidal_category-property/closed) and [coclosed](/symmetric_monoidal_category-property/coclosed) are dual to each other.
+
+A monoidal category has another dual, namely $(\C,\otimes^{\op},1)$, but for a symmetric monoidal category this is isomorphic to $(\C,\otimes,1)$.

database/data/categories/Ab_fg.yaml

@@ -23,6 +23,7 @@ satisfied_properties:
 
   - property: extremal generator
     proof: The group $\IZ$ is an extremal generator since it represents the forgetful functor to $\Set$ which is faithful and conservative.
+    label: Ab_fg_extremal_generator
 
   - property: essentially countable
     proof: Every finitely generated abelian group is isomorphic to a group of the form $\IZ^n / U$, where $n \in \IN$ and $U$ is a subgroup of $\IZ^n$. Since $\IZ^n$ is Noetherian as a $\IZ$-module, $U$ is finitely generated, hence the category $\Ab_\fg$ has only countably many objects up to isomorphism. Furthermore, for any objects $A \cong \IZ^n / U$ and $B \cong \IZ^m / T$, the hom-set $\Hom(A,B)$ is countable. Indeed, precomposition with the quotient map yields an injection $\Hom(A,B) \hookrightarrow \Hom(\IZ^n, B) \cong B^n$, and $B^n$ is countable.

database/data/categories/Top.yaml

@@ -43,6 +43,7 @@ satisfied_properties:
 
   - property: generator
     proof: The one-point space is a generator since it represents the forgetful functor $\Top \to \Set$.
+    label: top_generator
 
   - property: extremal cogenerator
     proof: >-

database/data/config.yaml

@@ -17,6 +17,8 @@ functor_tags:
 
 morphism_tags: []
 
+symmetric_monoidal_category_tags: []
+
 category_property_tags:
   - limits
   - colimits
@@ -46,6 +48,12 @@ morphism_property_tags:
   - types of epimorphisms
   - invertibility
 
+symmetric_monoidal_category_property_tags:
+  - tensor-colimit interaction
+  - tensor-limit interaction
+  - degeneracy
+  - misc
+
 relations:
   - relation: is
     negation: is not

database/data/macros.yaml

@@ -44,6 +44,7 @@
 \Hom: \operatorname{Hom}
 \HomInternal: \underline{\operatorname{Hom}}
 \End: \operatorname{End}
+\Bilin: \operatorname{Bilin}
 \Ob: \operatorname{Ob}
 \id: \operatorname{id}
 \card: \operatorname{card}

database/data/symmetric_monoidal_categories/1_tensor.yaml

@@ -0,0 +1,20 @@
+id: 1_tensor
+name: trivial symmetric monoidal category
+notation: $(1,\times,0)$
+underlying_category: '1'
+description: This is the terminal symmetric monoidal category. It is the <a href="/category/1">trivial category</a> $1$ equipped with its unique strict symmetric monoidal structure. The monoidal unit is the unique object $0$.
+nlab_link: null
+
+tags:
+  - category theory
+
+related: []
+
+satisfied_properties:
+  - property: trivial
+    proof: This holds by construction.
+
+  - property: strict
+    proof: This is obvious.
+
+unsatisfied_properties: []

database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml

@@ -0,0 +1,41 @@
+id: Ab_fg_tensor
+name: symmetric monoidal category of finitely generated abelian groups
+notation: $(\Ab_{\fg},\otimes,\IZ)$
+underlying_category: Ab_fg
+description: This is the full symmetric monoidal subcategory of $(\Ab,\otimes,\IZ)$ spanned by the finitely generated abelian groups. This is well-defined because $\IZ$ is finitely generated and the tensor product of two finitely generated abelian groups is finitely generated.
+nlab_link: null
+
+tags:
+  - algebra
+
+related:
+  - Ab_tensor
+  - FinVect_tensor
+
+satisfied_properties:
+  - property: closed
+    proof: Since <a href="/symmetric_monoidal_category/Ab_tensor">$(\Ab,\otimes,\IZ)$</a> is closed, it suffices to prove that for abelian groups $A,B$ with internal Hom $[A,B]$, if $A$ and $B$ are finitely generated, then $[A,B]$ is finitely generated. Since there is an epimorphism $\IZ^n \to A$, there is a monomorphism $[A,B] \to [\IZ^n,B] \cong B^n$. Since $B^n$ is finitely generated, the claim follows from the fact that subgroups of finitely generated abelian groups are finitely generated. (This also shows that the corresponding statement for finitely generated modules over a ring holds only when the ring is Noetherian.)
+
+  - property: well-pointed
+    proof: In fact, $\IZ$ is even an extremal generator of <a href="/category/Ab_fg">$\Ab_{\fg}$</a>.
+    references:
+      - Ab_fg_extremal_generator
+
+unsatisfied_properties:
+  - property: finitely complete
+    proof: The same counterexample as for <a href="/symmetric_monoidal_category/Ab_tensor">$(\Ab,\otimes,\IZ)$</a> works here.
+    references:
+      - Ab_tensor_not_fc
+
+  - property: strict
+    proof: The same argument as for <a href="/symmetric_monoidal_category/R-Mod_tensor">$(R{-}\Mod,\otimes,R)$</a> works here.
+    references:
+      - R-Mod_tensor_not_strict
+
+  - property: infinitary distributive
+    # TODO: automate this
+    proof: This is because <a href="/category/Ab_fg">$\Ab_{\fg}$</a> does not have coproducts.
+
+  - property: infinitary codistributive
+    # TODO: automate this
+    proof: This is because <a href="/category/Ab_fg">$\Ab_{\fg}$</a> does not have products.

database/data/symmetric_monoidal_categories/Ab_tensor.yaml

@@ -0,0 +1,20 @@
+id: Ab_tensor
+name: symmetric monoidal category of abelian groups
+notation: $(\Ab,\otimes,\IZ)$
+underlying_category: Ab
+description: This is the category of abelian groups equipped with the usual tensor product of abelian groups and the monoidal unit $\IZ$. It is the special case of <a href="/symmetric_monoidal_category/R-Mod_tensor_naf">$(R{-}\Mod,\otimes,R)$</a> where $R = \IZ$.
+nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+abelian+groups
+parent: R-Mod_tensor_naf
+
+tags:
+  - algebra
+
+related:
+  - Ab_fg_tensor
+
+satisfied_properties: []
+
+unsatisfied_properties:
+  - property: finitely complete
+    proof: 'The functor $\IZ/2\IZ \otimes - : \Ab \to \Ab$ does not preserve monomorphisms (see <a href="/functor/modulo-p">here</a>). For example, the injective homomorphism $2 : \IZ \to \IZ$ is mapped to the zero homomorphism $0 : \IZ/2\IZ \to \IZ/2\IZ$.'
+    label: Ab_tensor_not_fc

database/data/symmetric_monoidal_categories/Cat_cartesian.yaml

@@ -0,0 +1,24 @@
+id: Cat_cartesian
+name: cartesian symmetric monoidal category of small categories
+notation: $(\Cat,\times,1)$
+underlying_category: Cat
+description: Every category with finite products (also called a cartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the terminal object and $\otimes$ is the product $\times$. In this case, we apply this to the category $\Cat$ of small categories.
+nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category
+
+tags:
+  - category theory
+
+related:
+  - Set_cartesian
+
+satisfied_properties:
+  - property: cartesian
+    proof: This holds by definition.
+
+unsatisfied_properties:
+  - property: strict
+    # TODO: automate this with category_conclusions
+    proof: Whether the underlying monoidal category is strict depends on the specific construction of small categories and their products, but the symmetries cannot be identities, since otherwise $\Cat$ would be thin (see <a href="/category-implication/core-thin_products_thin">this proof</a>).
+
+  - property: well-pointed
+    proof: 'The terminal category is not a generator of $\Cat$ as it represents the functor $\Ob : \Cat \to \Set$, which is not faithful: A functor is not fully determined by its action on objects.'

database/data/symmetric_monoidal_categories/FinVect_tensor.yaml

@@ -0,0 +1,33 @@
+id: FinVect_tensor
+name: symmetric monoidal category of finite-dimensional vector spaces
+notation: $(\FinVect_K,\otimes,K)$
+underlying_category: FinVect
+description: This is the full symmetric monoidal subcategory of $(\Vect_K,\otimes,K)$ (see <a href="/symmetric_monoidal_category/R-Mod_tensor_af">here</a>) spanned by the finite-dimensional vector spaces.
+nlab_link: https://ncatlab.org/nlab/show/FinDimVect
+
+tags:
+  - algebra
+
+related:
+  - Ab_fg_tensor
+  - R-Mod_tensor_af
+
+satisfied_properties:
+  - property: closed
+    proof: This is because $(\Vect_K,\otimes,K)$ is closed and for finite-dimensional vector spaces $V,W$ also the vector space $[V,W]$ of linear maps is finite-dimensional (by elementary linear algebra).
+
+  - property: well-pointed
+    proof: In fact, $K$ is a generator of $\FinVect_K$, even in $\Vect_K$.
+    references:
+      - vect_extremal_generator
+
+  - property: self-dual
+    proof: From linear algebra we know that the dual vector space functor $V \mapsto V^*$ implements an equivalence $\FinVect \simeq \FinVect^{\op}$ with natural isomorphisms $K \cong K^*$ and $(V \otimes W)^* \cong V^* \otimes W^*$.
+
+unsatisfied_properties:
+  - property: strict
+    proof: 'Whether the underlying monoidal category is strict depends on the specific construction of vector spaces and their tensor products, but the symmetries cannot be identities. In fact, if $V$ is a finite-dimensional vector space, then the symmetry $\sigma_{V,V} : V \otimes V \to V \otimes V$ is the identity if and only if $V$ has dimension $\leq 1$.'
+
+  - property: infinitary distributive
+    # TODO: automate this
+    proof: This is because its underlying category $\FinVect$ does not have (infinite) coproducts.

database/data/symmetric_monoidal_categories/N+.yaml

@@ -0,0 +1,35 @@
+id: N+
+name: symmetric monoidal poset of natural numbers
+notation: $(\IN,\leq,+,0)$
+underlying_category: N
+description: We view the poset $(\IN,\leq)$ as a thin category and equip it with the strict symmetric monoidal structure defined by $a \otimes b := a + b$ and the monoidal unit $0$.
+nlab_link: https://ncatlab.org/nlab/show/monoidal+preorder
+
+tags:
+  - number theory
+
+related: []
+
+satisfied_properties:
+  - property: strict
+    proof: This follows by construction.
+
+  - property: coclosed
+    proof: >-
+      For $a \in \IN$ the order-preserving function $(\IN,\leq) \to (\IN,\leq)$, $x \mapsto x + a$, viewed as a functor between thin categories, has the left adjoint $y \mapsto \max(0, y - a)$ because for all $x,y \in \IN$ the following are equivalent:
+      $$y \leq x + a \iff y - a \leq x \iff \max(0, y - a) \leq x.$$
+
+unsatisfied_properties:
+  - property: cartesian
+    # TODO: automate this with category_conclusions
+    proof: This is simply because its underlying category <a href="/category/N">$(\IN,\leq)$</a> does not have finite products; it has no terminal object.
+
+  - property: codistributive
+    # TODO: automate this with category_conclusions
+    proof: This is simply because its underlying category <a href="/category/N">$(\IN,\leq)$</a> does not have finite products; it has no terminal object.
+
+  - property: distributive
+    proof: The functor $x \mapsto x \otimes 1 = x + 1$ does not preserve the initial object $0$.
+
+  - property: cocartesian
+    proof: Even though the monoidal unit is the initial object, the tensor product $a \otimes b = a + b$ is not given by the coproduct $\max(a,b)$ in $(\IN,\leq)$.

database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml

@@ -0,0 +1,33 @@
+id: R-Mod_tensor
+name: symmetric monoidal category of modules over a commutative ring
+notation: $(R{-}\Mod,\otimes,R)$
+underlying_category: R-Mod
+description: When $R$ is a commutative ring, we equip the category of left $R$-modules $R{-}\Mod$ with the usual symmetric monoidal structure, where $\otimes$ is the <a href="https://en.wikipedia.org/wiki/Tensor_product_of_modules" target="_blank">tensor product of modules</a> and the monoidal unit is $R$. The associator is defined by $(a \otimes b) \otimes c \mapsto a \otimes (b \otimes c)$, the left unitor maps $1 \otimes a \mapsto a$, the right unitor maps $a \otimes 1 \mapsto a$, and the symmetry maps $a \otimes b \mapsto b \otimes a$.
+nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules
+
+tags:
+  - algebra
+
+related:
+  - Ab_tensor
+
+satisfied_properties:
+  - property: closed
+    proof: >-
+      This is standard. If $A$ and $B$ are $R$-modules, let $[A,B]$ be the $R$-module whose underlying set is $\Hom(A,B)$, with pointwise operations (usually, this module is also denoted $\Hom(A,B)$, which can be confusing). Then there is a natural bijection
+      $$\Hom(C,[A,B]) \cong \Bilin(C,A;B) \cong \Hom(C \otimes A, B).$$
+
+  - property: well-pointed
+    proof: In fact, $R$ is a generator of $R{-}\Mod$, since it represents the forgetful functor $R{-}\Mod \to \Set$.
+
+unsatisfied_properties:
+  - property: infinitary codistributive
+    proof: The endofunctor $R^{\oplus \IN} \otimes -$ identifies with the copower functor $M \mapsto M^{\oplus \IN}$. It does not preserve countable products. Specifically, the canonical map $(R^{\IN})^{\oplus \IN} \to (R^{\oplus \IN})^{\IN}$ is injective, but not surjective.
+
+  - property: strict
+    proof: 'Whether the underlying monoidal category is strict depends on the specific construction of modules and their tensor products, but the symmetries cannot be identities. In fact, if $A$ is a finitely generated free $R$-module, then the symmetry $\sigma_{A,A} : A \otimes A \to A \otimes A$ is the identity if and only if $A$ has rank $\leq 1$.'
+    label: R-Mod_tensor_not_strict
+
+undecidable_properties:
+  - property: finitely complete
+    proof: This property holds if and only if every $R$-module is flat, i.e. that $R$ is <a href="https://en.wikipedia.org/wiki/Von_Neumann_regular_ring" target="_blank">absolutely flat</a>.

database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml

@@ -0,0 +1,19 @@
+id: R-Mod_tensor_af
+name: symmetric monoidal category of modules over an absolutely flat commutative ring
+notation: $(R{-}\Mod,\otimes,R)$
+underlying_category: R-Mod
+description: This is the special case of <a href="/symmetric_monoidal_category/R-Mod_tensor">this entry</a> where we assume that $R$ is <a href="https://en.wikipedia.org/wiki/Von_Neumann_regular_ring" target="_blank">absolutely flat</a> and non-zero. For example, every field has this property, so that this entry also includes the symmetric monoidal category of vector spaces.
+nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules
+parent: R-Mod_tensor
+
+tags:
+  - algebra
+
+related:
+  - FinVect_tensor
+
+satisfied_properties:
+  - property: finitely complete
+    proof: The underlying category is of course finitely complete. Apart from that, this property is exactly the assumption that $R$ is absolutely flat, meaning that every $R$-module $M$ is flat, so that $M \otimes -$ is left exact.
+
+unsatisfied_properties: []

database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml

@@ -0,0 +1,18 @@
+id: R-Mod_tensor_naf
+name: symmetric monoidal category of modules over a non-absolutely flat commutative ring
+notation: $(R{-}\Mod,\otimes,R)$
+underlying_category: R-Mod
+description: This is the special case of <a href="/symmetric_monoidal_category/R-Mod_tensor">$(R{-}\Mod,\otimes,R)$</a> where $R$ is a commutative ring that is not <a href="https://en.wikipedia.org/wiki/Von_Neumann_regular_ring" target="_blank">absolutely flat</a>.
+nlab_link: https://ncatlab.org/nlab/show/tensor+product+of+modules
+parent: R-Mod_tensor
+
+tags:
+  - algebra
+
+related: []
+
+satisfied_properties: []
+
+unsatisfied_properties:
+  - property: finitely complete
+    proof: Since we assume that $R$ is not absolutely flat, there is some $R$-module $M$ that is not flat. This means that the endofunctor $M \otimes -$ is not left exact.