diff --git a/.cspell.json b/.cspell.json index 716885cf7..fab514581 100644 --- a/.cspell.json +++ b/.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", diff --git a/DATABASE.md b/DATABASE.md index c72992db3..67f01133f 100644 --- a/DATABASE.md +++ b/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: diff --git a/README.md b/README.md index 07c4c84ea..182922b8d 100644 --- a/README.md +++ b/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. diff --git a/content/dual-properties.md b/content/dual-properties.md index 39a1276f4..b6dfddb7b 100644 --- a/content/dual-properties.md +++ b/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)$. diff --git a/database/data/categories/Ab_fg.yaml b/database/data/categories/Ab_fg.yaml index daa552fab..5ee7021d0 100644 --- a/database/data/categories/Ab_fg.yaml +++ b/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. diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index d86852e3b..fc5304d84 100644 --- a/database/data/categories/Top.yaml +++ b/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: >- diff --git a/database/data/config.yaml b/database/data/config.yaml index 58025140f..36b076414 100644 --- a/database/data/config.yaml +++ b/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 diff --git a/database/data/macros.yaml b/database/data/macros.yaml index 652f1e185..b7639653e 100644 --- a/database/data/macros.yaml +++ b/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} diff --git a/database/data/symmetric_monoidal_categories/1_tensor.yaml b/database/data/symmetric_monoidal_categories/1_tensor.yaml new file mode 100644 index 000000000..e6b5d28f4 --- /dev/null +++ b/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 trivial category $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: [] diff --git a/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml b/database/data/symmetric_monoidal_categories/Ab_fg_tensor.yaml new file mode 100644 index 000000000..28107ba32 --- /dev/null +++ b/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 $(\Ab,\otimes,\IZ)$ 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 $\Ab_{\fg}$. + references: + - Ab_fg_extremal_generator + +unsatisfied_properties: + - property: finitely complete + proof: The same counterexample as for $(\Ab,\otimes,\IZ)$ works here. + references: + - Ab_tensor_not_fc + + - property: strict + proof: The same argument as for $(R{-}\Mod,\otimes,R)$ works here. + references: + - R-Mod_tensor_not_strict + + - property: infinitary distributive + # TODO: automate this + proof: This is because $\Ab_{\fg}$ does not have coproducts. + + - property: infinitary codistributive + # TODO: automate this + proof: This is because $\Ab_{\fg}$ does not have products. diff --git a/database/data/symmetric_monoidal_categories/Ab_tensor.yaml b/database/data/symmetric_monoidal_categories/Ab_tensor.yaml new file mode 100644 index 000000000..527788229 --- /dev/null +++ b/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 $(R{-}\Mod,\otimes,R)$ 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 here). 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 diff --git a/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml b/database/data/symmetric_monoidal_categories/Cat_cartesian.yaml new file mode 100644 index 000000000..41fb0ef2c --- /dev/null +++ b/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 this proof). + + - 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.' diff --git a/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml b/database/data/symmetric_monoidal_categories/FinVect_tensor.yaml new file mode 100644 index 000000000..503dfa6f7 --- /dev/null +++ b/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 here) 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. diff --git a/database/data/symmetric_monoidal_categories/N+.yaml b/database/data/symmetric_monoidal_categories/N+.yaml new file mode 100644 index 000000000..dcc695d57 --- /dev/null +++ b/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 $(\IN,\leq)$ 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 $(\IN,\leq)$ 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)$. diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor.yaml new file mode 100644 index 000000000..e833197a8 --- /dev/null +++ b/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 tensor product of modules 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 absolutely flat. diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor_af.yaml new file mode 100644 index 000000000..50e60dab8 --- /dev/null +++ b/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 this entry where we assume that $R$ is absolutely flat 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: [] diff --git a/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml b/database/data/symmetric_monoidal_categories/R-Mod_tensor_naf.yaml new file mode 100644 index 000000000..f2eb58d17 --- /dev/null +++ b/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 $(R{-}\Mod,\otimes,R)$ where $R$ is a commutative ring that is not absolutely flat. +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. diff --git a/database/data/symmetric_monoidal_categories/Set_cartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml new file mode 100644 index 000000000..4225e650a --- /dev/null +++ b/database/data/symmetric_monoidal_categories/Set_cartesian.yaml @@ -0,0 +1,31 @@ +id: Set_cartesian +name: cartesian symmetric monoidal category of sets +notation: $(\Set,\times,1)$ +underlying_category: Set +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 $\Set$. +nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category + +tags: + - set theory + +related: + - Top_cartesian + - Cat_cartesian + +satisfied_properties: + - property: cartesian + proof: This holds by definition. + + - property: well-pointed + proof: We know that the singleton set is even an extremal generator of $\Set$. + references: + - set_extremal_generator + +unsatisfied_properties: + - property: trivial + # TODO: automate this with category_conclusions + proof: This is because $\Set$ is not trivial. + + - property: strict + # TODO: automate this with category_conclusions + proof: Whether the underlying monoidal category is strict depends on the specific construction of sets and their products (see also MSE/4468970), but the symmetries cannot be identities, since otherwise $\Set$ would be thin (see this proof). diff --git a/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml new file mode 100644 index 000000000..a7003fcac --- /dev/null +++ b/database/data/symmetric_monoidal_categories/Set_cocartesian.yaml @@ -0,0 +1,28 @@ +id: Set_cocartesian +name: cocartesian symmetric monoidal category of sets +notation: $(\Set,\sqcup,0)$ +underlying_category: Set +description: Every category with finite coproducts (also called a cocartesian category) can be endowed with a symmetric monoidal structure, where $1$ is the initial object and $\otimes$ is the coproduct $\sqcup$. In this case, we apply this to the category $\Set$. +nlab_link: https://ncatlab.org/nlab/show/cocartesian+monoidal+category + +tags: + - set theory + +related: + - Set_cartesian + +satisfied_properties: + - property: cocartesian + 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 sets and their coproducts, but the symmetries cannot be identities, since otherwise $\Set$ would be thin (see this proof, dualized). + + - property: codistributive + proof: If $A$ is a non-empty set, the functor $A \sqcup - $ does not preserve the terminal object. + + - property: well-pointed + # TODO: automate this with category_conclusions + proof: The empty set is clearly not a generator of $\Set$ since otherwise it would be thin. diff --git a/database/data/symmetric_monoidal_categories/Top_cartesian.yaml b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml new file mode 100644 index 000000000..d8f1659d6 --- /dev/null +++ b/database/data/symmetric_monoidal_categories/Top_cartesian.yaml @@ -0,0 +1,29 @@ +id: Top_cartesian +name: cartesian symmetric monoidal category of topological spaces +notation: $(\Top,\times,1)$ +underlying_category: Top +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 $\Top$. +nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category + +tags: + - topology + +related: + - Set_cartesian + +satisfied_properties: + - property: cartesian + proof: This holds by definition. + + - property: well-pointed + proof: We know that the one-point space is a generator of $\Top$. + references: + - top_generator + +unsatisfied_properties: + - property: strict + # TODO: automate this with category_conclusions + proof: Whether the underlying monoidal category is strict depends on the specific construction of sets and their products, but the symmetries cannot be identities, since otherwise $\Top$ would be thin (see this proof). + + - property: finitely cocomplete + proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve coequalizers, see here or MSE/2969372.' diff --git a/database/data/symmetric_monoidal_category_implications/closed.yaml b/database/data/symmetric_monoidal_category_implications/closed.yaml new file mode 100644 index 000000000..1b83ed28d --- /dev/null +++ b/database/data/symmetric_monoidal_category_implications/closed.yaml @@ -0,0 +1,56 @@ +# results on closed symmetric monoidal categories + +- id: closed_cartesian_symmetric_monoidal + assumptions: + - cartesian + mapped_assumptions: + underlying_category: + - cartesian closed + conclusions: + - closed + proof: This is just the definition of a cartesian closed category. + is_equivalence: false + +- id: when_closed_implies_cocomplete + assumptions: + - closed + mapped_assumptions: + underlying_category: + - cocomplete + conclusions: + - cocomplete + proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves colimits. + is_equivalence: false + +- id: when_closed_implies_finitely_cocomplete + assumptions: + - closed + mapped_assumptions: + underlying_category: + - finitely cocomplete + conclusions: + - finitely cocomplete + proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves finite colimits. + is_equivalence: false + +- id: when_closed_implies_distributive + assumptions: + - closed + mapped_assumptions: + underlying_category: + - finite coproducts + conclusions: + - distributive + proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves finite coproducts. + is_equivalence: false + +- id: when_closed_implies_infinitary_distributive + assumptions: + - closed + mapped_assumptions: + underlying_category: + - coproducts + conclusions: + - infinitary distributive + proof: Each functor $A \otimes -$ is a left adjoint and therefore preserves coproducts. + is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml new file mode 100644 index 000000000..02a7f4167 --- /dev/null +++ b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml @@ -0,0 +1,70 @@ +# results concerning (co)complete symmetric monoidal categories and related notions + +- id: cocomplete_implies_finitely_cocomplete + assumptions: + - cocomplete + conclusions: + - finitely cocomplete + - infinitary distributive + proof: This is trivial. + is_equivalence: false + +- id: finitely_cocomplete_consequences + assumptions: + - finitely cocomplete + conclusions: + - distributive + proof: This is trivial. + is_equivalence: false + +- id: infinitary_distributive_consequence + assumptions: + - infinitary distributive + conclusions: + - distributive + proof: This is trivial. + is_equivalence: false + +- id: distributive_cartesian + assumptions: + - cartesian + mapped_assumptions: + underlying_category: + - distributive + conclusions: + - distributive + proof: This is just the definition of a distributive category. + # TODO: make this an equivalence when we have category_conclusions + is_equivalence: false + +- id: infinitary_distributive_cartesian + assumptions: + - cartesian + mapped_assumptions: + underlying_category: + - infinitary distributive + conclusions: + - infinitary distributive + proof: This is just the definition of an infinitary distributive category. + # TODO: make this an equivalence when we have category_conclusions + is_equivalence: false + +- id: cartesian_never_complete + assumptions: + - cartesian + - codistributive + conclusions: + - trivial + proof: In a codistributive symmetric monoidal category, for every object $X$, the functor $X \otimes -$ preserves the terminal object $1$. But since the symmetric monoidal structure is assumed to be cartesian, $1$ is the monoidal unit, so $1 = X \otimes 1 = X$. + is_equivalence: false + +- id: preadditive_codistributive_criterion + assumptions: + - distributive + mapped_assumptions: + underlying_category: + - biproducts + conclusions: + - codistributive + proof: This follows from this result on functors. + is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_implications/misc.yaml b/database/data/symmetric_monoidal_category_implications/misc.yaml new file mode 100644 index 000000000..26f25512a --- /dev/null +++ b/database/data/symmetric_monoidal_category_implications/misc.yaml @@ -0,0 +1,31 @@ +# misc results on symmetric monoidal categories + +- id: trivial_is_everything + assumptions: + - trivial + conclusions: + - cartesian + - closed + - cocomplete + - self-dual + proof: This is trivial. + is_equivalence: false + +- id: trivial_is_well_pointed + # we need this separately since well-pointed currently has no dual + assumptions: + - trivial + conclusions: + - well-pointed + proof: This is trivial. + is_equivalence: false + +- id: thin_is_well_pointed + assumptions: [] + mapped_assumptions: + underlying_category: + - thin + conclusions: + - well-pointed + proof: In a thin category, every object is a generator for trivial reasons. + is_equivalence: false diff --git a/database/data/symmetric_monoidal_category_properties/cartesian.yaml b/database/data/symmetric_monoidal_category_properties/cartesian.yaml new file mode 100644 index 000000000..1859bddd8 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/cartesian.yaml @@ -0,0 +1,10 @@ +id: cartesian +relation: is +description: 'A symmetric monoidal category is called cartesian when its underlying category has finite products and the symmetric monoidal structure is induced by these finite products; that is, $A \otimes B = A \times B$, and so on.' +nlab_link: https://ncatlab.org/nlab/show/cartesian+monoidal+category +invariant_under_equivalences: true +dual: cocartesian +related: [] + +tags: + - misc diff --git a/database/data/symmetric_monoidal_category_properties/closed.yaml b/database/data/symmetric_monoidal_category_properties/closed.yaml new file mode 100644 index 000000000..b2ec5a1c8 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/closed.yaml @@ -0,0 +1,10 @@ +id: closed +relation: is +description: 'A symmetric monoidal category is called closed when, for every object $A$, the endofunctor $- \otimes A$ has a right adjoint $[A,-]$. Thus, we have natural bijections $\Hom(B \otimes A,C) \cong \Hom(B,[A,C])$.' +nlab_link: https://ncatlab.org/nlab/show/closed+monoidal+category +invariant_under_equivalences: true +dual: coclosed +related: [] + +tags: + - misc diff --git a/database/data/symmetric_monoidal_category_properties/cocartesian.yaml b/database/data/symmetric_monoidal_category_properties/cocartesian.yaml new file mode 100644 index 000000000..745eaff94 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/cocartesian.yaml @@ -0,0 +1,10 @@ +id: cocartesian +relation: is +description: 'A symmetric monoidal category is called cocartesian when its underlying category has finite coproducts and the symmetric monoidal structure is induced by these finite coproducts; that is, $A \otimes B = A \sqcup B$, and so on.' +nlab_link: https://ncatlab.org/nlab/show/cocartesian+monoidal+category +invariant_under_equivalences: true +dual: cartesian +related: [] + +tags: + - misc diff --git a/database/data/symmetric_monoidal_category_properties/coclosed.yaml b/database/data/symmetric_monoidal_category_properties/coclosed.yaml new file mode 100644 index 000000000..693377c48 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/coclosed.yaml @@ -0,0 +1,10 @@ +id: coclosed +relation: is +description: 'A symmetric monoidal category is called coclosed when, for every object $A$, the endofunctor $- \otimes A$ has a left adjoint. This property is not very common, but we have included it because of its dual property.' +nlab_link: null +invariant_under_equivalences: true +dual: closed +related: [] + +tags: + - misc diff --git a/database/data/symmetric_monoidal_category_properties/cocomplete.yaml b/database/data/symmetric_monoidal_category_properties/cocomplete.yaml new file mode 100644 index 000000000..c5053c1a4 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/cocomplete.yaml @@ -0,0 +1,12 @@ +id: cocomplete +relation: is +description: 'A symmetric monoidal category is called cocomplete when its underlying category is cocomplete and, for every object $A$, the endofunctor $A \otimes -$ is cocontinuous. Of course, then the endofunctor $- \otimes A$ is also cocontinuous. There is no need for a more complicated term such as "symmetric monoidally cocomplete" if one is careful to distinguish between a symmetric monoidal category and its underlying category.' +nlab_link: https://ncatlab.org/nlab/show/monoidally+cocomplete+category +invariant_under_equivalences: true +dual: complete +related: + - finitely cocomplete + - infinitary distributive + +tags: + - tensor-colimit interaction diff --git a/database/data/symmetric_monoidal_category_properties/codistributive.yaml b/database/data/symmetric_monoidal_category_properties/codistributive.yaml new file mode 100644 index 000000000..7992feafa --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/codistributive.yaml @@ -0,0 +1,12 @@ +id: codistributive +relation: is +description: 'A symmetric monoidal category is called codistributive when its underlying category has finite products and, for every object $A$, the endofunctor $A \otimes -$ preserves finite products. There should be no confusion with the closely related notion of a codistributive category as long as we distinguish carefully between a symmetric monoidal category and its underlying category.' +nlab_link: null +invariant_under_equivalences: true +dual: distributive +related: + - infinitary codistributive + - finitely complete + +tags: + - tensor-limit interaction diff --git a/database/data/symmetric_monoidal_category_properties/complete.yaml b/database/data/symmetric_monoidal_category_properties/complete.yaml new file mode 100644 index 000000000..5efc535cd --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/complete.yaml @@ -0,0 +1,11 @@ +id: complete +relation: is +description: 'A symmetric monoidal category is called complete when its underlying category is complete and, for every object $A$, the endofunctor $A \otimes -$ is continuous. Of course, then the endofunctor $- \otimes A$ is also continuous. There is no need for a more complicated term such as "symmetric monoidally complete" if one is careful to distinguish between a symmetric monoidal category and its underlying category.' +nlab_link: null +invariant_under_equivalences: true +dual: cocomplete +related: + - finitely complete + +tags: + - tensor-limit interaction diff --git a/database/data/symmetric_monoidal_category_properties/distributive.yaml b/database/data/symmetric_monoidal_category_properties/distributive.yaml new file mode 100644 index 000000000..6f3b73cac --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/distributive.yaml @@ -0,0 +1,12 @@ +id: distributive +relation: is +description: 'A symmetric monoidal category is called distributive when its underlying category has finite coproducts and, for every object $A$, the endofunctor $A \otimes -$ preserves finite coproducts. There should be no confusion with the closely related notion of a distributive category as long as we distinguish carefully between a symmetric monoidal category and its underlying category.' +nlab_link: https://ncatlab.org/nlab/show/distributive+monoidal+category +invariant_under_equivalences: true +dual: codistributive +related: + - infinitary distributive + - finitely cocomplete + +tags: + - tensor-colimit interaction diff --git a/database/data/symmetric_monoidal_category_properties/finitely cocomplete.yaml b/database/data/symmetric_monoidal_category_properties/finitely cocomplete.yaml new file mode 100644 index 000000000..9a9f2e6d1 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/finitely cocomplete.yaml @@ -0,0 +1,11 @@ +id: finitely cocomplete +relation: is +description: 'A symmetric monoidal category is called finitely cocomplete when its underlying category is finitely cocomplete and, for every object $A$, the endofunctor $A \otimes -$ preserves finite colimits (that is, it is right exact). Of course, then the endofunctor $- \otimes A$ also preserves finite colimits. There is no need for a more complicated term such as "symmetric monoidally finitely cocomplete" if one is careful to distinguish between a symmetric monoidal category and its underlying category.' +nlab_link: null +invariant_under_equivalences: true +dual: finitely complete +related: + - cocomplete + +tags: + - tensor-colimit interaction diff --git a/database/data/symmetric_monoidal_category_properties/finitely complete.yaml b/database/data/symmetric_monoidal_category_properties/finitely complete.yaml new file mode 100644 index 000000000..38d627885 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/finitely complete.yaml @@ -0,0 +1,11 @@ +id: finitely complete +relation: is +description: 'A symmetric monoidal category is called finitely complete when its underlying category is finitely complete and, for every object $A$, the endofunctor $A \otimes -$ preserves finite limits (that is, it is left exact). Of course, then the endofunctor $- \otimes A$ also preserves finite limits. There is no need for a more complicated term such as "symmetric monoidally finitely complete" if one is careful to distinguish between a symmetric monoidal category and its underlying category.' +nlab_link: null +invariant_under_equivalences: true +dual: finitely cocomplete +related: + - complete + +tags: + - tensor-limit interaction diff --git a/database/data/symmetric_monoidal_category_properties/infinitary codistributive.yaml b/database/data/symmetric_monoidal_category_properties/infinitary codistributive.yaml new file mode 100644 index 000000000..34771a2e0 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/infinitary codistributive.yaml @@ -0,0 +1,12 @@ +id: infinitary codistributive +relation: is +description: 'A symmetric monoidal category is called infinitary codistributive when its underlying category has products and, for every object $A$, the endofunctor $A \otimes -$ preserves products. There should be no confusion with the closely related notion of an infinitary codistributive category as long as we distinguish carefully between a symmetric monoidal category and its underlying category.' +nlab_link: null +invariant_under_equivalences: true +dual: infinitary distributive +related: + - codistributive + - complete + +tags: + - tensor-limit interaction diff --git a/database/data/symmetric_monoidal_category_properties/infinitary distributive.yaml b/database/data/symmetric_monoidal_category_properties/infinitary distributive.yaml new file mode 100644 index 000000000..ac9b5ff7b --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/infinitary distributive.yaml @@ -0,0 +1,12 @@ +id: infinitary distributive +relation: is +description: 'A symmetric monoidal category is called infinitary distributive when its underlying category has coproducts and, for every object $A$, the endofunctor $A \otimes -$ preserves coproducts. There should be no confusion with the closely related notion of an infinitary distributive category as long as we distinguish carefully between a symmetric monoidal category and its underlying category.' +nlab_link: https://ncatlab.org/nlab/show/distributive+monoidal+category +invariant_under_equivalences: true +dual: infinitary codistributive +related: + - distributive + - cocomplete + +tags: + - tensor-colimit interaction diff --git a/database/data/symmetric_monoidal_category_properties/self-dual.yaml b/database/data/symmetric_monoidal_category_properties/self-dual.yaml new file mode 100644 index 000000000..4c45c9a64 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/self-dual.yaml @@ -0,0 +1,10 @@ +id: self-dual +relation: is +description: 'A symmetric monoidal category $(\C,\otimes,1)$ is self-dual when it is equivalent to its dual symmetric monoidal category $(\C^{\op},\otimes,1)$.' +nlab_link: null +invariant_under_equivalences: true +dual: self-dual +related: [] + +tags: + - misc diff --git a/database/data/symmetric_monoidal_category_properties/strict.yaml b/database/data/symmetric_monoidal_category_properties/strict.yaml new file mode 100644 index 000000000..dd6084fbc --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/strict.yaml @@ -0,0 +1,10 @@ +id: strict +relation: is +description: 'A symmetric monoidal category is called strict when its associator, symmetry, left unitor, and right unitor are identities. A strict symmetric monoidal category is simply a commutative monoid object in $(\Cat^+,\times,1)$.' +nlab_link: https://ncatlab.org/nlab/show/strict+monoidal+category +invariant_under_equivalences: false +dual: strict +related: [] + +tags: + - degeneracy diff --git a/database/data/symmetric_monoidal_category_properties/trivial.yaml b/database/data/symmetric_monoidal_category_properties/trivial.yaml new file mode 100644 index 000000000..e6810dda6 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/trivial.yaml @@ -0,0 +1,10 @@ +id: trivial +relation: is +description: 'A symmetric monoidal category is trivial when it is equivalent to the terminal symmetric monoidal category. This is equivalent to the condition that its underlying category is trivial.' +nlab_link: null +invariant_under_equivalences: true +dual: trivial +related: [] + +tags: + - degeneracy diff --git a/database/data/symmetric_monoidal_category_properties/well-pointed.yaml b/database/data/symmetric_monoidal_category_properties/well-pointed.yaml new file mode 100644 index 000000000..734b206b4 --- /dev/null +++ b/database/data/symmetric_monoidal_category_properties/well-pointed.yaml @@ -0,0 +1,10 @@ +id: well-pointed +relation: is +description: 'A symmetric monoidal category $(\C,\otimes,1)$ is called well-pointed if the monoidal unit $1$ is a generator. Equivalently, the functor $\Hom(1,-) : \C \to \Set^+$ is faithful. The terminology is taken from Categories for Quantum Theory by Heunen-Vicari, Def. 1.12.' +nlab_link: null +invariant_under_equivalences: true +dual: null +related: [] + +tags: + - misc diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index 6414f57bc..cf73970a7 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -5,7 +5,27 @@ CREATE TABLE structure_types ( INSERT INTO structure_types (type) VALUES ('category'), ('functor'), - ('morphism'); + ('morphism'), + ('symmetric_monoidal_category'); + + +CREATE TABLE structure_maps ( + map TEXT NOT NULL, + type TEXT NOT NULL, + mapped_type TEXT NOT NULL, + PRIMARY KEY (map, type, mapped_type), + UNIQUE (map, type), + FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, + FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE +); + +INSERT INTO structure_maps + (map, type, mapped_type) +VALUES + ('domain', 'functor', 'category'), + ('codomain', 'functor', 'category'), + ('category', 'morphism', 'category'), + ('underlying_category', 'symmetric_monoidal_category', 'category'); CREATE TABLE structures ( id TEXT PRIMARY KEY, @@ -60,21 +80,4 @@ CREATE TABLE structure_tag_assignments ( PRIMARY KEY (structure_id, type, tag), FOREIGN KEY (structure_id, type) REFERENCES structures (id, type) ON DELETE CASCADE, FOREIGN KEY (tag, type) REFERENCES structure_tags (tag, type) ON DELETE CASCADE -); - -CREATE TABLE structure_maps ( - map TEXT NOT NULL, - type TEXT NOT NULL, - mapped_type TEXT NOT NULL, - PRIMARY KEY (map, type, mapped_type), - UNIQUE (map, type), - FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE -); - -INSERT INTO structure_maps - (map, type, mapped_type) -VALUES - ('domain', 'functor', 'category'), - ('codomain', 'functor', 'category'), - ('category', 'morphism', 'category'); \ No newline at end of file +); \ No newline at end of file diff --git a/database/schema/009_symmetric-monoidal-categories.sql b/database/schema/009_symmetric-monoidal-categories.sql new file mode 100644 index 000000000..b9ceab78e --- /dev/null +++ b/database/schema/009_symmetric-monoidal-categories.sql @@ -0,0 +1,17 @@ +CREATE TABLE symmetric_monoidal_categories ( + id TEXT PRIMARY KEY, + underlying_category TEXT NOT NULL, + FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, + FOREIGN KEY (underlying_category) REFERENCES categories (id) ON DELETE CASCADE +); + +CREATE TRIGGER trg_symmetric_monoidal_category_type_check +BEFORE INSERT ON symmetric_monoidal_categories +BEGIN + SELECT + CASE + WHEN + (SELECT type FROM structures WHERE id = NEW.id) != 'symmetric_monoidal_category' + THEN RAISE(ABORT, 'Symmetric monoidal categories must have type "symmetric_monoidal_category"') + END; +END; \ No newline at end of file diff --git a/database/scripts/deduce-implications.ts b/database/scripts/deduce-implications.ts index b9457cd52..6eafa4966 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -3,7 +3,8 @@ import { are_equal_sets, parse_nested_json_set, parse_json_set, - devlog + devlog, + remove_underscores } from '$shared/utils' import { get_client } from '$shared/db' @@ -13,7 +14,7 @@ const db = get_client({ readonly: false }) * Clears all deduced implications. This is done before the deduction starts. */ export function clear_deduced_implications(type: StructureType) { - console.info(`\n--- Deduce ${type} implications ---`) + console.info(`\n--- Deduce ${remove_underscores(type)} implications ---`) db.prepare(`DELETE FROM implications WHERE is_deduced = TRUE AND type = ?`).run(type) } @@ -155,7 +156,7 @@ export function create_dualized_implications(type: StructureType) { } } - devlog(`Deduced ${count} ${type} implications by duality`) + devlog(`Deduced ${count} ${remove_underscores(type)} implications by duality`) }) insert_duals() @@ -200,12 +201,14 @@ export function create_self_dual_implications(type: StructureType) { `) for (const p of relevant_props) { - const implication_id = `self-dual_${p.id}` + const implication_id = `self-dual_${p.id}_${type}` implication_insert.run(implication_id, type) assumption_insert.run(implication_id, p.id, type) assumption_insert.run(implication_id, 'self-dual', type) conclusion_insert.run(implication_id, p.dual, type) } - devlog(`Deduced ${relevant_props.length} ${type} implications by self-duality`) + devlog( + `Deduced ${relevant_props.length} ${remove_underscores(type)} implications by self-duality` + ) } diff --git a/database/scripts/deduce-structure-properties.ts b/database/scripts/deduce-structure-properties.ts index 478a94cc5..73fe7f020 100644 --- a/database/scripts/deduce-structure-properties.ts +++ b/database/scripts/deduce-structure-properties.ts @@ -20,7 +20,7 @@ import { type StructureMeta } from './utils/structures' import { get_normalized_implications, NormalizedImplication } from '$shared/implications' -import { devlog } from '$shared/utils' +import { devlog, remove_underscores } from '$shared/utils' /** * Deduce satisfied properties for a given structure from given ones @@ -296,7 +296,7 @@ function inherit_properties_from_parents(db: Database, type: StructureType) { * by using the stored implications. */ export function deduce_properties_for_structures(type: StructureType) { - console.info(`\n--- Deduce ${type} properties ---`) + console.info(`\n--- Deduce ${remove_underscores(type)} properties ---`) const db = get_client({ readonly: false }) diff --git a/database/scripts/deduce.ts b/database/scripts/deduce.ts index 7ba360a2d..3f406d3f2 100644 --- a/database/scripts/deduce.ts +++ b/database/scripts/deduce.ts @@ -34,4 +34,10 @@ function deduce() { create_dualized_implications('morphism') deduce_properties_for_structures('morphism') restrict_morphism_properties() + + // --- symmetric monoidal categories + clear_deduced_implications('symmetric_monoidal_category') + create_dualized_implications('symmetric_monoidal_category') + create_self_dual_implications('symmetric_monoidal_category') + deduce_properties_for_structures('symmetric_monoidal_category') } diff --git a/database/scripts/expected-data/decided-symmetric-monoidal-categories.json b/database/scripts/expected-data/decided-symmetric-monoidal-categories.json new file mode 100644 index 000000000..6c7f5e3a8 --- /dev/null +++ b/database/scripts/expected-data/decided-symmetric-monoidal-categories.json @@ -0,0 +1 @@ +["Set_cartesian", "Ab_tensor", "N+"] diff --git a/database/scripts/proof-length.ts b/database/scripts/proof-length.ts index ebfde75c5..81b14b411 100644 --- a/database/scripts/proof-length.ts +++ b/database/scripts/proof-length.ts @@ -1,5 +1,6 @@ import { STRUCTURE_TYPES, type StructureType } from '$shared/config' import { get_client } from '$shared/db' +import { remove_underscores } from '$shared/utils' get_client const db = get_client({ readonly: true }) @@ -39,7 +40,7 @@ function report_long_property_proofs(type: StructureType) { if (!long_proofs.length) return - console.info(`\n--- Long property proofs (type: ${type}) ---`) + console.info(`\n--- Long property proofs (type: ${remove_underscores(type)}) ---`) for (const { id, property, length } of long_proofs) { console.warn( @@ -65,7 +66,7 @@ function report_long_implication_proofs(type: StructureType) { if (!long_proofs.length) return - console.info(`\n--- Long implication proofs (type: ${type}) ---`) + console.info(`\n--- Long implication proofs (type: ${remove_underscores(type)}) ---`) for (const { id, length } of long_proofs) { console.warn( diff --git a/database/scripts/redundancies.ts b/database/scripts/redundancies.ts index bf3520a7e..f8fb0d2dd 100644 --- a/database/scripts/redundancies.ts +++ b/database/scripts/redundancies.ts @@ -8,6 +8,7 @@ import { } from '$shared/implications' import { deduce_properties, refute_properties } from '$shared/deduction.utils' import { get_structures } from './utils/structures' +import { remove_underscores } from '$shared/utils' const db = get_client({ readonly: true }) @@ -29,7 +30,9 @@ function check_redundancies() { * No error is thrown intentionally. */ function check_redundant_property_assignments(type: StructureType) { - console.info(`\n--- Check redundant ${type} property assignments ---`) + console.info( + `\n--- Check redundant ${remove_underscores(type)} property assignments ---` + ) const implications = get_normalized_implications(db, type) diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index fb05670ba..b07bfa014 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -9,7 +9,8 @@ import type { SpecialMorphismRuleYaml, StructureYaml, PropertyYaml, - MorphismYaml + MorphismYaml, + SymmetricMonoidalCategoryYaml } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' @@ -43,6 +44,20 @@ function seed() { seed_properties({ type: 'morphism', folder: 'morphism-properties' }) seed_implications({ type: 'morphism', folder: 'morphism-implications' }) seed_structures({ type: 'morphism', folder: 'morphisms', extra: insert_morphism }) + + seed_properties({ + type: 'symmetric_monoidal_category', + folder: 'symmetric_monoidal_category_properties' + }) + seed_implications({ + type: 'symmetric_monoidal_category', + folder: 'symmetric_monoidal_category_implications' + }) + seed_structures({ + type: 'symmetric_monoidal_category', + folder: 'symmetric_monoidal_categories', + extra: insert_symmetric_monoidal_category + }) } /** @@ -332,29 +347,30 @@ function insert_category(category: CategoryYaml) { * Inserts the data of a functor that is specific to functors. */ function insert_functor(functor: FunctorYaml) { - const functor_insert = db.prepare( + db.prepare( `INSERT INTO functors (id, domain, codomain, left_adjoint) VALUES (?, ?, ?, ?)` - ) - - functor_insert.run( - functor.id, - functor.domain, - functor.codomain, - functor.left_adjoint || null - ) + ).run(functor.id, functor.domain, functor.codomain, functor.left_adjoint || null) } /** * Inserts the data of a morphism that is specific to morphisms. */ function insert_morphism(morphism: MorphismYaml) { - const morphism_insert = db.prepare( + db.prepare( `INSERT INTO morphisms (id, category) VALUES (?, ?)` - ) + ).run(morphism.id, morphism.category) +} - morphism_insert.run(morphism.id, morphism.category) +/** + * Inserts the data of a symmetric monoidal category that is specific to symmetric monoidal categories. + */ +function insert_symmetric_monoidal_category(s: SymmetricMonoidalCategoryYaml) { + db.prepare( + `INSERT INTO symmetric_monoidal_categories (id, underlying_category) + VALUES (?, ?)` + ).run(s.id, s.underlying_category) } /** diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 9708df817..b55f67897 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -11,7 +11,8 @@ import forget_vector_expected from './expected-data/forget_vector.json' import decided_categories from './expected-data/decided-categories.json' import decided_functors from './expected-data/decided-functors.json' import decided_morphisms from './expected-data/decided-morphisms.json' -import { capitalize, devlog } from '$shared/utils' +import decided_symmetric_monoidal_categories from './expected-data/decided-symmetric-monoidal-categories.json' +import { capitalize, devlog, remove_underscores } from '$shared/utils' import { get_client } from '$shared/db' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' import fs from 'node:fs' @@ -57,6 +58,14 @@ function execute_tests() { test_positivity('id_G', 'morphism') test_decided_structures(decided_morphisms, 'morphism') + + devlog('\n--- Test symmetric monoidal categories ---') + + test_positivity('1_tensor', 'symmetric_monoidal_category') + test_decided_structures( + decided_symmetric_monoidal_categories, + 'symmetric_monoidal_category' + ) } catch (err) { if (err instanceof Error) { console.error(err.message) @@ -88,7 +97,9 @@ function test_mutual_structure_duals(type: StructureType) { for (const id in dict) { const dual = dict[id] if (dual && dict[dual] !== id) { - throw new Error(`❌ Found non-mutual ${type} duality: ${id}, ${dual}`) + throw new Error( + `❌ Found non-mutual ${remove_underscores(type)} duality: ${id}, ${dual}` + ) } } @@ -110,11 +121,13 @@ function test_positivity(structure_id: string, type: StructureType) { if (unsatisfied_props.length > 0) { throw new Error( - `❌ The ${type} ${structure_id} has ${unsatisfied_props.length} unsatisfied properties, but it should have 0.` + `❌ The ${remove_underscores(type)} ${structure_id} has ${unsatisfied_props.length} unsatisfied properties, but it should have 0.` ) } - devlog(`✅ The ${type} ${structure_id} has no unsatisfied properties`) + devlog( + `✅ The ${remove_underscores(type)} ${structure_id} has no unsatisfied properties` + ) } /** @@ -142,7 +155,7 @@ function test_mutual_property_duals(type: StructureType) { } } - devlog(`✅ ${capitalize(type)} properties are mutually dual`) + devlog(`✅ ${capitalize(remove_underscores(type))} properties are mutually dual`) } /** @@ -165,7 +178,7 @@ function test_decided_structures(structure_ids: string[], type: StructureType) { if (unknown_properties.length > 0) { throw new Error( - `❌ Found unknown properties of ${structure_id}:\n${unknown_properties.join(', ')}.\nEvery property needs to be decided for this ${type}.` + `❌ Found unknown properties of ${structure_id}:\n${unknown_properties.join(', ')}.\nEvery property needs to be decided for this ${remove_underscores(type)}.` ) } diff --git a/database/scripts/utils/implications.ts b/database/scripts/utils/implications.ts index f48cfd039..90778783a 100644 --- a/database/scripts/utils/implications.ts +++ b/database/scripts/utils/implications.ts @@ -2,6 +2,7 @@ import type { PropertyMeta } from './properties' import { type StructureType } from '$shared/config' import { get_property_label } from '$shared/property.utils' import { type NormalizedImplication } from '$shared/implications' +import { remove_underscores } from '$shared/utils' function get_assumption_string( implication: NormalizedImplication, @@ -18,14 +19,14 @@ function get_assumption_string( `${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${get_property_label(assumption)}` ) .join(' and ') - : `is a ${type}` + : `is a ${remove_underscores(type)}` if (!implication.mapped_assumptions) return own const mapped = Object.entries(implication.mapped_assumptions) .map( ([map, props]) => - `and the ${map} has the required properties (${Array.from(props!).join(', ')})` + `and the ${remove_underscores(map)} has the required properties (${Array.from(props!).join(', ')})` ) .join(', ') diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index ffb930478..dfc372d82 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -3,9 +3,11 @@ export type ConfigYaml = { category_tags: string[] functor_tags: string[] morphism_tags: string[] + symmetric_monoidal_category_tags: string[] category_property_tags: string[] functor_property_tags: string[] morphism_property_tags: string[] + symmetric_monoidal_category_property_tags: string[] relations: { relation: string negation: string @@ -78,6 +80,10 @@ export type MorphismYaml = StructureYaml & { category: string } +export type SymmetricMonoidalCategoryYaml = StructureYaml & { + underlying_category: string +} + export type PropertyYaml = { id: string relation: string diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index b6b91f6f4..88978aaba 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -13,12 +13,12 @@ export type StructureMeta = { /** * Dictionary associating to every structure type the name of the table. - * Currently, this is the same as the plural. */ const TABLES: Record = { category: 'categories', functor: 'functors', - morphism: 'morphisms' + morphism: 'morphisms', + symmetric_monoidal_category: 'symmetric_monoidal_categories' } /** diff --git a/shared/config.ts b/shared/config.ts index 9e4a2311f..68f649355 100644 --- a/shared/config.ts +++ b/shared/config.ts @@ -1,4 +1,9 @@ -export const STRUCTURE_TYPES = ['category', 'functor', 'morphism'] as const +export const STRUCTURE_TYPES = [ + 'category', + 'functor', + 'morphism', + 'symmetric_monoidal_category' +] as const export type StructureType = (typeof STRUCTURE_TYPES)[number] @@ -6,10 +11,14 @@ export function is_structure_type(txt: string): txt is StructureType { return (STRUCTURE_TYPES as readonly string[]).includes(txt) } -export const STRUCTURE_TYPES_WITH_DUALS: StructureType[] = ['category'] +export const STRUCTURE_TYPES_WITH_DUALS: StructureType[] = [ + 'category', + 'symmetric_monoidal_category' +] export const PLURALS: Record = { category: 'categories', functor: 'functors', - morphism: 'morphisms' + morphism: 'morphisms', + symmetric_monoidal_category: 'symmetric monoidal categories' } diff --git a/shared/utils.ts b/shared/utils.ts index 0cb45d731..7b30aea78 100644 --- a/shared/utils.ts +++ b/shared/utils.ts @@ -49,6 +49,10 @@ export function normalize_text(txt: string) { .replace(/\p{Diacritic}/gu, '') } +export function remove_underscores(txt: string) { + return txt.replaceAll('_', ' ') +} + export function parse_json_set(json: string): Set { return new Set(JSON.parse(json)) } diff --git a/src/components/Selection.svelte b/src/components/Selection.svelte index 4d52070dd..7315016d6 100644 --- a/src/components/Selection.svelte +++ b/src/components/Selection.svelte @@ -3,6 +3,7 @@ import Chip from './Chip.svelte' import { get_comparison_score } from '$lib/client/utils' import type { Snippet } from 'svelte' + import { remove_underscores } from '$shared/utils' type Props = { allowed_items: readonly string[] @@ -130,7 +131,7 @@
0 && !is_valid(item)} type="text" diff --git a/src/components/StructureSelector.svelte b/src/components/StructureSelector.svelte index f36a7943b..279c81f90 100644 --- a/src/components/StructureSelector.svelte +++ b/src/components/StructureSelector.svelte @@ -47,6 +47,7 @@ select { font-size: 1rem; + field-sizing: content; } @media (width <= 600px) { diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 6aca366c6..35710c3d4 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -141,6 +141,7 @@ export type CategorySpecificDisplay = { special_morphisms: SpecialMorphism[] stored_functors: StructureShort[] stored_morphisms: StructureShort[] + stored_symmetric_monoidal_categories: StructureShort[] } export type FunctorSpecificDisplay = { @@ -163,3 +164,9 @@ export type MorphismSpecificDisplay = { category_name: string category_notation: string } + +export type SymmetricMonoidalCategorySpecificDisplay = { + underlying_category: string + underlying_category_name: string + underlying_category_notation: string +} diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index 4d9ff7bd4..af8d44212 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -39,6 +39,8 @@ export function fetch_category(id: string) { ) .all(id) + // TODO: make this more systematic by looping over the structure_maps + const stored_functors = db .prepare<[string, string], StructureShort>( `SELECT f.id, s.name @@ -59,13 +61,24 @@ export function fetch_category(id: string) { ) .all(id) + const stored_symmetric_monoidal_categories = db + .prepare<[string], StructureShort>( + `SELECT c.id, s.name + FROM symmetric_monoidal_categories c + INNER JOIN structures s ON s.id = c.id + WHERE c.underlying_category = ? + ORDER BY lower(s.name)` + ) + .all(id) + return { type: 'category' as const, ...category, special_objects, special_morphisms, stored_functors, - stored_morphisms + stored_morphisms, + stored_symmetric_monoidal_categories } } diff --git a/src/lib/server/fetchers/symmetric_monoidal_category.ts b/src/lib/server/fetchers/symmetric_monoidal_category.ts new file mode 100644 index 000000000..89cb454c3 --- /dev/null +++ b/src/lib/server/fetchers/symmetric_monoidal_category.ts @@ -0,0 +1,21 @@ +import type { SymmetricMonoidalCategorySpecificDisplay } from '$lib/commons/types' +import { db } from '$lib/server/db' +import { error } from '@sveltejs/kit' + +export function fetch_symmetric_monoidal_category(id: string) { + const s = db + .prepare<[string], SymmetricMonoidalCategorySpecificDisplay>( + `SELECT + c.id AS underlying_category, + c.name AS underlying_category_name, + c.notation AS underlying_category_notation + FROM symmetric_monoidal_categories s + INNER JOIN structures AS c ON c.id = s.underlying_category + WHERE s.id = ?` + ) + .get(id) + + if (!s) error(404, `Could not find symmetric monoidal category with ID '${id}'`) + + return { type: 'symmetric_monoidal_category' as const, ...s } +} diff --git a/src/pages/CategoryDetailPage.svelte b/src/pages/CategoryDetailPage.svelte index b343ace3e..d07dc1efb 100644 --- a/src/pages/CategoryDetailPage.svelte +++ b/src/pages/CategoryDetailPage.svelte @@ -59,6 +59,7 @@ {/snippet} {#snippet footer()} + {#if data.stored_functors.length}

Functors

@@ -90,5 +91,24 @@
{/if} + + {#if data.stored_symmetric_monoidal_categories} +
+

Symmetric monoidal categories

+ +

+ The database has stored + {pluralize(data.stored_symmetric_monoidal_categories.length, { + one: '{count} symmetric monoidal category', + other: '{count} symmetric monoidal categories' + })} + based on the {data.structure.name}. +

+ +
+ {/if} {/snippet} diff --git a/src/pages/ImplicationListPage.svelte b/src/pages/ImplicationListPage.svelte index 3cd1e9bed..58f48a8c4 100644 --- a/src/pages/ImplicationListPage.svelte +++ b/src/pages/ImplicationListPage.svelte @@ -5,7 +5,12 @@ import MetaData from '$components/MetaData.svelte' import SearchFilter from '$components/SearchFilter.svelte' import SuggestionForm from '$components/SuggestionForm.svelte' - import { capitalize, normalize_text, pluralize } from '$shared/utils' + import { + capitalize, + normalize_text, + pluralize, + remove_underscores + } from '$shared/utils' import type { ImplicationDisplay, StructureType } from '$lib/commons/types' import { faInfoCircle } from '@fortawesome/free-solid-svg-icons' import type { Snippet } from 'svelte' @@ -45,9 +50,9 @@ ) - + -

{capitalize(type)} implications

+

{capitalize(remove_underscores(type))} implications

diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index e6c4711d0..06f29490b 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -2,7 +2,7 @@ import StructureList from '$components/StructureList.svelte' import MetaData from '$components/MetaData.svelte' import SuggestionForm from '$components/SuggestionForm.svelte' - import { pluralize } from '$shared/utils' + import { pluralize, remove_underscores } from '$shared/utils' import { get_property_url } from '$shared/property.utils' import type { ImplicationDisplay, @@ -35,11 +35,11 @@

Claim: {#if has_additional_assumptions} - Given a {type} + Given a {remove_underscores(type)} {#each Object.entries(implication.mapped_assumptions) as [map, set], ind} {#if set} whose - {map} + {remove_underscores(map)} {#each set as property, index} {property_relation_dict[mapped_types[map]][property]} {property}

{pluralize(structures.length, { - one: `Show {count} ${type} using this implication`, + one: `Show {count} ${remove_underscores(type)} using this implication`, other: `Show {count} ${PLURALS[type]} using this implication` })} diff --git a/src/pages/PropertyPage.svelte b/src/pages/PropertyPage.svelte index ce92f952d..248a8d3ca 100644 --- a/src/pages/PropertyPage.svelte +++ b/src/pages/PropertyPage.svelte @@ -4,7 +4,7 @@ import ImplicationList from '$components/ImplicationList.svelte' import MetaData from '$components/MetaData.svelte' import SuggestionForm from '$components/SuggestionForm.svelte' - import { pluralize } from '$shared/utils' + import { pluralize, remove_underscores } from '$shared/utils' import { get_property_url } from '$shared/property.utils' import { faInfoCircle } from '@fortawesome/free-solid-svg-icons' import Fa from 'svelte-fa' @@ -110,7 +110,7 @@

{pluralize(examples.length, { - one: `There is {count} ${type} with this property.`, + one: `There is {count} ${remove_underscores(type)} with this property.`, other: `There are {count} ${PLURALS[type]} with this property.` })}

@@ -121,7 +121,7 @@

{pluralize(counterexamples.length, { - one: `There is {count} ${type} without this property.`, + one: `There is {count} ${remove_underscores(type)} without this property.`, other: `There are {count} ${PLURALS[type]} without this property.` })}

@@ -133,7 +133,7 @@

{pluralize(undecidable_structures.length, { - one: `There is {count} ${type} for which it cannot be decided if this property is satisfied or not.`, + one: `There is {count} ${remove_underscores(type)} for which it cannot be decided if this property is satisfied or not.`, other: `There are {count} ${PLURALS[type]} for which it cannot be decided if this property is satisfied or not.` })}

@@ -145,7 +145,7 @@

{pluralize(unknown_structures.length, { - one: `There is {count} ${type} for which the database has no information on whether it satisfies this property.`, + one: `There is {count} ${remove_underscores(type)} for which the database has no information on whether it satisfies this property.`, other: `There are {count} ${PLURALS[type]} for which the database has no information on whether they satisfy this property.` })} {#if unknown_structures.length > 0} diff --git a/src/pages/SearchResultsPage.svelte b/src/pages/SearchResultsPage.svelte index d8b4f3be7..4539b5e6e 100644 --- a/src/pages/SearchResultsPage.svelte +++ b/src/pages/SearchResultsPage.svelte @@ -4,7 +4,7 @@ import { encode_property_ID, get_property_url } from '$shared/property.utils' import MetaData from '$components/MetaData.svelte' import { SEARCH_SEPARATOR } from '$lib/commons/search.config' - import { pluralize } from '$shared/utils' + import { pluralize, remove_underscores } from '$shared/utils' import Fa from 'svelte-fa' import { faWarning } from '@fortawesome/free-solid-svg-icons' import type { SearchResults, StructureType } from '$lib/commons/types' @@ -88,7 +88,7 @@ {#if !contradiction}

{pluralize(found_structures.length, { - one: `Found {count} ${type}`, + one: `Found {count} ${remove_underscores(type)}`, other: found_structures.length === 0 ? `Found {count} ${PLURALS[type]}. Try to dualize the search.` diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index 4d2e8c1de..fd486540c 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -16,6 +16,7 @@ StructureType } from '$lib/commons/types' import type { Snippet } from 'svelte' + import { remove_underscores } from '$shared/utils' type Props = { type: StructureType @@ -110,7 +111,7 @@ {#if structure.dual_structure_id}

  • - Dual {type}: + Dual {remove_underscores(type)}:

    List of {PLURALS[type]}

    - {#if type === 'morphism'} + {#if type === 'morphism' || type === 'symmetric_monoidal_category'}

    - The morphism application is still in its early stages. More morphisms will be added - soon. + The {remove_underscores(type)} application is still in its early stages. More {PLURALS[ + type + ]} will be added soon.

    {/if} @@ -47,7 +48,7 @@

    {pluralize(searched_structures.length, { - one: `Found {count} ${type}`, + one: `Found {count} ${remove_underscores(type)}`, other: `Found {count} ${PLURALS[type]}` })}

    diff --git a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte new file mode 100644 index 000000000..6213f9c07 --- /dev/null +++ b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte @@ -0,0 +1,22 @@ + + + + {#snippet definition()} +
  • + Underlying category: + + {data.underlying_category_name} + +
    • + {/snippet} + diff --git a/src/routes/+page.svelte b/src/routes/+page.svelte index 1dbe1211c..09133dcd7 100644 --- a/src/routes/+page.svelte +++ b/src/routes/+page.svelte @@ -21,8 +21,11 @@

    CatDat provides a growing collection of categorical structures such as categories, - functors, and - morphisms. Built by and for those who love + functors, + morphisms, and + symmetric monoidal categories. Built by and for those who love category theory . diff --git a/src/routes/[type]-implications/+page.svelte b/src/routes/[type]-implications/+page.svelte index 46c8dbcaf..21549bb98 100644 --- a/src/routes/[type]-implications/+page.svelte +++ b/src/routes/[type]-implications/+page.svelte @@ -53,6 +53,13 @@ overview of the relationships between the various types of epimorphisms and monomorphisms.

    + {:else if data.type === 'symmetric_monoidal_category'} +

    + *Deductions from these implications are automatically incorporated into + each symmetric monoidal category whenever applicable. Moreover, + implications are automatically dualized when the corresponding dual + properties exist. +

    {/if}

    diff --git a/src/routes/[type]-search/+page.svelte b/src/routes/[type]-search/+page.svelte index e19c21d44..ba746c332 100644 --- a/src/routes/[type]-search/+page.svelte +++ b/src/routes/[type]-search/+page.svelte @@ -9,7 +9,9 @@ '/category-search/results?satisfied=finitely_complete~pointed&unsatisfied=complete', functor: '/functor-search/results?satisfied=continuous&unsatisfied=cocontinuous', morphism: - '/morphism-search/results?satisfied=monomorphism~epimorphism&unsatisfied=isomorphism' + '/morphism-search/results?satisfied=monomorphism~epimorphism&unsatisfied=isomorphism', + symmetric_monoidal_category: + '/symmetric_monoidal_category-search/results?satisfied=cocomplete&unsatisfied=cartesian' } @@ -27,5 +29,9 @@ For example, you can look for morphisms that are monomorphisms and epimorphisms, but no isomorphisms. + {:else if data.type === 'symmetric_monoidal_category'} + For example, you can + look + for symmetric monoidal categories that are cocomplete, but not cartesian. {/if} diff --git a/src/routes/[type]/[id]/+page.server.ts b/src/routes/[type]/[id]/+page.server.ts index 665af5a3d..58af8b25c 100644 --- a/src/routes/[type]/[id]/+page.server.ts +++ b/src/routes/[type]/[id]/+page.server.ts @@ -6,11 +6,13 @@ import { fetch_category } from '$lib/server/fetchers/category' import { fetch_functor } from '$lib/server/fetchers/functor' import { fetch_morphism } from '$lib/server/fetchers/morphism' import { add_math, strip_math } from '$shared/utils' +import { fetch_symmetric_monoidal_category } from '$lib/server/fetchers/symmetric_monoidal_category' const special_fetchers = { category: fetch_category, functor: fetch_functor, - morphism: fetch_morphism + morphism: fetch_morphism, + symmetric_monoidal_category: fetch_symmetric_monoidal_category } export const load = (event) => { diff --git a/src/routes/[type]/[id]/+page.svelte b/src/routes/[type]/[id]/+page.svelte index e6f33eab0..da567a1e3 100644 --- a/src/routes/[type]/[id]/+page.svelte +++ b/src/routes/[type]/[id]/+page.svelte @@ -2,10 +2,13 @@ import CategoryDetailPage from '$pages/CategoryDetailPage.svelte' import FunctorDetailPage from '$pages/FunctorDetailPage.svelte' import MorphismDetailPage from '$pages/MorphismDetailPage.svelte' + import SymmetricMonoidalCategoryDetailPage from '$pages/SymmetricMonoidalCategoryDetailPage.svelte' let { data } = $props() + + {#if data.special_structure_data.type === 'category'} {/if} @@ -17,3 +20,10 @@ {#if data.special_structure_data.type === 'morphism'} {/if} + +{#if data.special_structure_data.type === 'symmetric_monoidal_category'} + +{/if} diff --git a/src/routes/missing/+page.svelte b/src/routes/missing/+page.svelte index 7294f45cb..eeb00017e 100644 --- a/src/routes/missing/+page.svelte +++ b/src/routes/missing/+page.svelte @@ -5,7 +5,7 @@ import { get_property_url } from '$shared/property.utils' import { PLURALS } from '$shared/config' import { STRUCTURE_TYPES } from '$shared/config' - import { capitalize, pluralize } from '$shared/utils' + import { capitalize, pluralize, remove_underscores } from '$shared/utils' const { data } = $props() @@ -60,7 +60,7 @@ {#if pairs.length > 0}

    -

    Indistinguishable {type} pairs

    +

    Indistinguishable {remove_underscores(type)} pairs

    {pluralize(pairs.length, { @@ -93,13 +93,14 @@ {@const combinations = data.missing_combinations[type]}

    -

    Missing {type} combinations

    +

    Missing {remove_underscores(type)} combinations

    {#if combinations.length}

    - Among the consistent {type} property combinations of the form p ∧ ¬q, - the following are not yet witnessed by a {type} in the database or its dual. - If some of these combinations are + Among the consistent {remove_underscores(type)} property combinations of the + form p ∧ ¬q, the following are not yet witnessed by a {remove_underscores( + type + )} in the database or its dual. If some of these combinations are inconsistent, this indicates that some implication is missing.

    @@ -121,8 +122,9 @@ {:else}

    - Every consistent {type} property combination of the form p ∧ ¬q is witnessed - by a {type} in the database or its dual. 🎉 + Every consistent {remove_underscores(type)} property combination of the form + p ∧ ¬q is witnessed by a {remove_underscores(type)} in the database + or its dual. 🎉

    —

    diff --git a/tests/missing.spec.ts b/tests/missing.spec.ts index 08b68807d..00d0e59d9 100644 --- a/tests/missing.spec.ts +++ b/tests/missing.spec.ts @@ -31,9 +31,11 @@ test('user can see categories with missing data', async ({ page }) => { }) ).toBeVisible() - const categories_section = page.locator('section', { - hasText: 'Categories with unknown properties' - }) + const categories_section = page + .locator('section', { + hasText: 'Categories with unknown properties' + }) + .first() await expect(categories_section).toBeVisible() @@ -112,7 +114,7 @@ test('user cannot see any missing functor combinations', async ({ page }) => { await expect(combinations_section).toBeVisible() await expect(combinations_section).toHaveText( - /.+Every consistent functor property combination.+is witnessed/ + /Every consistent functor property combination[\s\S]+is witnessed/ ) }) @@ -127,6 +129,6 @@ test('user cannot see any missing morphism combinations', async ({ page }) => { await expect(combinations_section).toBeVisible() await expect(combinations_section).toHaveText( - /.+Every consistent morphism property combination.+is witnessed/ + /.+Every consistent morphism property combination[\s\S]+is witnessed/ ) }) diff --git a/tests/structure_selector.spec.ts b/tests/structure_selector.spec.ts index f62d76a63..4187cdc7e 100644 --- a/tests/structure_selector.spec.ts +++ b/tests/structure_selector.spec.ts @@ -91,3 +91,44 @@ test('morphisms are selected on a morphism route', async ({ page }) => { await expect(selector).toBeVisible() await expect(selector).toHaveValue('morphism') }) + +test('user can switch to symmetric monoidal categories', async ({ page }) => { + await page.goto('/', { waitUntil: 'networkidle' }) + + const selector = page + .getByRole('combobox', { + name: 'Structure', + exact: true + }) + .first() + + await expect(selector).toBeVisible() + await selector.selectOption('symmetric_monoidal_category') + + await expect(selector).toHaveValue('symmetric_monoidal_category') + + await expect(page).toHaveURL('/symmetric_monoidal_category-list') + + await expect( + page.getByRole('heading', { + name: 'List of symmetric monoidal categories', + exact: true + }) + ).toBeVisible() +}) + +test('symmetric monoidal categories are selected on a symmetric monoidal category route', async ({ + page +}) => { + await page.goto('/symmetric_monoidal_category-properties') + + const selector = page + .getByRole('combobox', { + name: 'Structure', + exact: true + }) + .first() + + await expect(selector).toBeVisible() + await expect(selector).toHaveValue('symmetric_monoidal_category') +}) diff --git a/tests/symmetric_monoidal_categories.spec.ts b/tests/symmetric_monoidal_categories.spec.ts new file mode 100644 index 000000000..0ac246da3 --- /dev/null +++ b/tests/symmetric_monoidal_categories.spec.ts @@ -0,0 +1,82 @@ +import { test, expect } from '@playwright/test' + +// This test file does not cover all features of symmetric monoidal categories, +// but only a selection. The other features are covered sufficiently by the +// test cases for the other types of categorical structures. + +test('user can navigate to a symmetric monoidal category', async ({ page }) => { + await page.goto('/') + + await page + .getByRole('link', { + name: 'symmetric monoidal categories', + exact: true + }) + .first() + .click() + + await expect( + page.getByRole('heading', { + name: 'List of symmetric monoidal categories', + exact: true + }) + ).toBeVisible() + + await expect(page).toHaveURL('/symmetric_monoidal_category-list') + + await page + .getByRole('link', { + name: 'symmetric monoidal category of abelian groups', + exact: true + }) + .click() + + await expect( + page.getByRole('heading', { + name: 'symmetric monoidal category of abelian groups', + exact: true + }) + ).toBeVisible() + + await expect(page).toHaveURL('/symmetric_monoidal_category/Ab_tensor') +}) + +test('user can view symmetric monoidal category details', async ({ page }) => { + await page.goto('/symmetric_monoidal_category/Ab_tensor') + + await expect( + page.getByRole('heading', { + name: 'symmetric monoidal category of abelian groups', + exact: true + }) + ).toBeVisible() + + await expect(page.getByText('tensor product of abelian groups')).toBeVisible() + await expect(page.getByText('is closed')).toBeVisible() + await expect(page.getByText('is cocomplete')).toBeVisible() + await expect(page.getByText('is not strict')).toBeVisible() + await expect(page.getByText('is not cartesian')).toBeVisible() +}) + +test('user can navigate to the underlying category', async ({ page }) => { + await page.goto('/symmetric_monoidal_category/Set_cartesian', { + waitUntil: 'networkidle' + }) + + await page + .getByRole('link', { + name: 'category of sets', + exact: true + }) + .first() + .click() + + await expect( + page.getByRole('heading', { + name: 'category of sets', + exact: true + }) + ).toBeVisible() + + await expect(page).toHaveURL('/category/Set') +})