diff --git a/DATABASE.md b/DATABASE.md index fe58e40ea..f994351f5 100644 --- a/DATABASE.md +++ b/DATABASE.md @@ -14,13 +14,6 @@ The `structures` table stores data that is common to all types of categorical st - `structure_types` -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: - `property_assignments` @@ -34,7 +27,7 @@ These tables are abstracted through the `implications_view` view. Functor implications may also depend on properties of the domain or codomain category. Likewise, morphism implications may depend on properties of the ambient category. Such dependencies are stored in the following table: -- `mapped_assumptions` +- `associated_assumptions` Additional tables are available. For a complete overview, see the diagram below. @@ -110,6 +103,6 @@ to check for redundant assignments of properties to categorical structures. ## Diagram -This is the database schema as of 13.08.2026; changes may occur. +This is the database schema as of 15.08.2026; changes may occur. -database diagram +database diagram diff --git a/database/data/functor-implications/adjoints.yaml b/database/data/functor-implications/adjoints.yaml index 5fbc20eee..2df2c48dc 100644 --- a/database/data/functor-implications/adjoints.yaml +++ b/database/data/functor-implications/adjoints.yaml @@ -9,7 +9,7 @@ - id: saft assumptions: - continuous - mapped_assumptions: + associated_assumptions: domain: - cogenerating set - complete @@ -34,7 +34,7 @@ - id: representable_right_adjoint assumptions: - representable - mapped_assumptions: + associated_assumptions: domain: - locally essentially small - coproducts @@ -45,7 +45,7 @@ - id: initial_object_as_left_adjoint assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - initial object codomain: diff --git a/database/data/functor-implications/limits preservation.yaml b/database/data/functor-implications/limits preservation.yaml index ba2e0549e..86cbef071 100644 --- a/database/data/functor-implications/limits preservation.yaml +++ b/database/data/functor-implications/limits preservation.yaml @@ -29,7 +29,7 @@ assumptions: - preserves terminal objects - preserves binary products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -41,7 +41,7 @@ assumptions: - preserves equalizers - preserves products - mapped_assumptions: + associated_assumptions: domain: - products conclusions: @@ -53,7 +53,7 @@ assumptions: - cofinitary - left exact - mapped_assumptions: + associated_assumptions: domain: - finitely complete conclusions: @@ -65,7 +65,7 @@ assumptions: - cofinitary - preserves finite products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -99,7 +99,7 @@ assumptions: - preserves equalizers - preserves finite products - mapped_assumptions: + associated_assumptions: domain: - finite products conclusions: @@ -128,7 +128,7 @@ assumptions: - preserves coreflexive equalizers - preserves binary products - mapped_assumptions: + associated_assumptions: domain: - binary products conclusions: @@ -139,7 +139,7 @@ - id: mono-preserving_criterion assumptions: - preserves regular monomorphisms - mapped_assumptions: + associated_assumptions: domain: - mono-regular conclusions: @@ -150,7 +150,7 @@ - id: regular-mono-preserving_criterion assumptions: - preserves monomorphisms - mapped_assumptions: + associated_assumptions: codomain: - mono-regular conclusions: @@ -161,7 +161,7 @@ - id: another_regular-mono-preserving_criterion assumptions: - preserves coreflexive equalizers - mapped_assumptions: + associated_assumptions: domain: - pushouts conclusions: @@ -172,7 +172,7 @@ - id: zero_preserving_condition assumptions: - preserves terminal objects - mapped_assumptions: + associated_assumptions: domain: - pointed codomain: @@ -185,7 +185,7 @@ - id: biproduct_preserving_condition assumptions: - preserves finite coproducts - mapped_assumptions: + associated_assumptions: domain: - biproducts codomain: @@ -233,7 +233,7 @@ - id: trivial_functors_continuous assumptions: [] - mapped_assumptions: + associated_assumptions: codomain: - trivial conclusions: @@ -243,7 +243,7 @@ - id: automatically_preserve_equalizers assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - regular-subobject-trivial conclusions: @@ -254,7 +254,7 @@ - id: trivial_coreflexive_equalizer_preservation # TODO: rework this once we add "split-epi-trivial" assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - regular-quotient-trivial conclusions: @@ -264,7 +264,7 @@ - id: thin_binary_product_preservation assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - thin - semi-strongly connected diff --git a/database/data/functor-implications/misc.yaml b/database/data/functor-implications/misc.yaml index 5bb0c681c..6ff468de1 100644 --- a/database/data/functor-implications/misc.yaml +++ b/database/data/functor-implications/misc.yaml @@ -11,7 +11,7 @@ assumptions: - conservative - preserves equalizers - mapped_assumptions: + associated_assumptions: domain: - equalizers conclusions: @@ -30,7 +30,7 @@ - id: faithful_with_balanced_domain assumptions: - faithful - mapped_assumptions: + associated_assumptions: domain: - balanced conclusions: @@ -101,7 +101,7 @@ - id: surjective_functor_to_core_connected_category assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - inhabited codomain: @@ -113,7 +113,7 @@ - id: right_invertible_functor_to_trivial_category assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - inhabited codomain: @@ -126,7 +126,7 @@ - id: full_functor_to_trivial_category # TODO: add the converse once we have category_conclusions assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - strongly connected codomain: @@ -138,7 +138,7 @@ - id: functor_conservative_on_groupoids assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - groupoid conclusions: @@ -148,7 +148,7 @@ - id: automatic_ess_injective_functors assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - core-connected conclusions: @@ -158,7 +158,7 @@ - id: automatic_full_on_isos_functors assumptions: [] - mapped_assumptions: + associated_assumptions: domain: - core-connected codomain: @@ -172,7 +172,7 @@ # TODO: rework this once we add "split-mono trivial" assumptions: - dominant - mapped_assumptions: + associated_assumptions: codomain: - regular-subobject-trivial conclusions: @@ -182,7 +182,7 @@ - id: automatic_preserves_mono assumptions: [] - mapped_assumptions: + associated_assumptions: codomain: - left cancellative conclusions: diff --git a/database/data/functor-implications/monadic.yaml b/database/data/functor-implications/monadic.yaml index 9742136f3..591fb5c80 100644 --- a/database/data/functor-implications/monadic.yaml +++ b/database/data/functor-implications/monadic.yaml @@ -13,7 +13,7 @@ - right adjoint - conservative - preserves reflexive coequalizers - mapped_assumptions: + associated_assumptions: domain: - reflexive coequalizers conclusions: diff --git a/database/data/functors/abelianization.yaml b/database/data/functors/abelianization.yaml index 2bd138246..a20bd0f44 100644 --- a/database/data/functors/abelianization.yaml +++ b/database/data/functors/abelianization.yaml @@ -6,6 +6,7 @@ codomain: Ab description: This functor maps a group $G$ to its abelianization $G^{\ab} \coloneqq G/[G,G]$. nlab_link: https://ncatlab.org/nlab/show/abelianization left_adjoint: null +right_adjoint: forget_abelian tags: - algebra diff --git a/database/data/functors/binary_coproduct_sets.yaml b/database/data/functors/binary_coproduct_sets.yaml index e2866b182..05d01e848 100644 --- a/database/data/functors/binary_coproduct_sets.yaml +++ b/database/data/functors/binary_coproduct_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$. It is an example of a right-invertible left adjoint functor which is not a reflector. nlab_link: null left_adjoint: null +right_adjoint: diagonal_sets tags: - set theory diff --git a/database/data/functors/binary_product_sets.yaml b/database/data/functors/binary_product_sets.yaml index 00ba6d450..b4639bbe9 100644 --- a/database/data/functors/binary_product_sets.yaml +++ b/database/data/functors/binary_product_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a pair of sets $(X,Y)$ to their product $X \times Y$. It is an example of a right-invertible right adjoint functor which is not a coreflector. nlab_link: null left_adjoint: diagonal_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/brauer_group.yaml b/database/data/functors/brauer_group.yaml index 10636f298..9888bc89c 100644 --- a/database/data/functors/brauer_group.yaml +++ b/database/data/functors/brauer_group.yaml @@ -6,6 +6,7 @@ codomain: Ab description: The Brauer group $\Br(K)$ of a field $K$ consists of equivalence classes of central simple algebras over $K$, where $A \sim B$ iff $A \otimes_K M_n(K) \cong B \otimes_K M_n(K)$ for some $n \geq 0$. The group structure is given by $[A] \cdot [B] \coloneqq [A \otimes_K B]$, $1 \coloneqq [K]$ and $[A]^{-1} \coloneqq [A^{\op}]$. A homomorphism $K \to L$ induces the homomorphism $\Br(K) \to \Br(L)$ defined by $[A] \mapsto [A \otimes_K L]$. nlab_link: https://ncatlab.org/nlab/show/Brauer+group left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/continuous-functions.yaml b/database/data/functors/continuous-functions.yaml index 20a1942de..75a0322dc 100644 --- a/database/data/functors/continuous-functions.yaml +++ b/database/data/functors/continuous-functions.yaml @@ -6,6 +6,7 @@ codomain: CAlg(R) # TODO: specify that R is IR description: 'This functor maps a topological space $X$ to the commutative $\IR$-algebra $C(X)$ of continuous functions $X \to \IR$. A continuous map $f : X \to Y$ is mapped to the algebra homomorphism $f^* : C(Y) \to C(X)$, $u \mapsto u \circ f$.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/countable_copower_sets.yaml b/database/data/functors/countable_copower_sets.yaml index bd01ca6c3..a75a9cda8 100644 --- a/database/data/functors/countable_copower_sets.yaml +++ b/database/data/functors/countable_copower_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to the product $\IN \times X$, which can also be seen as the copower $\IN \otimes X = \coprod_{n \in \IN} X$. It is an example of a polynomial functor. nlab_link: null left_adjoint: null +right_adjoint: sequences_sets tags: - set theory diff --git a/database/data/functors/diagonal_sets.yaml b/database/data/functors/diagonal_sets.yaml index 87ce3358e..72fc8410e 100644 --- a/database/data/functors/diagonal_sets.yaml +++ b/database/data/functors/diagonal_sets.yaml @@ -6,6 +6,7 @@ codomain: SetxSet description: 'Every category $\C$ has a (binary) diagonal functor $\Delta : \C \to \C^2$, $X \mapsto (X,X)$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/diagonal+functor left_adjoint: binary_coproduct_sets +right_adjoint: binary_product_sets tags: - set theory diff --git a/database/data/functors/discrete_topology.yaml b/database/data/functors/discrete_topology.yaml index 398260266..79a914b45 100644 --- a/database/data/functors/discrete_topology.yaml +++ b/database/data/functors/discrete_topology.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a set $X$ to the discrete topological space $D(X) \coloneqq (X, P(X))$ in which every subset is open. It is a typical example of a fully faithful functor that preserves finite but does not preserve infinite products. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology left_adjoint: null +right_adjoint: forget_topology tags: - topology diff --git a/database/data/functors/doubling_sets.yaml b/database/data/functors/doubling_sets.yaml index 56727bfd3..79e27eea9 100644 --- a/database/data/functors/doubling_sets.yaml +++ b/database/data/functors/doubling_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to its double $2 X \coloneqq X + X$. It is a simple example of a polynomial functor. nlab_link: null left_adjoint: null +right_adjoint: squaring_sets tags: - set theory diff --git a/database/data/functors/empty_sets.yaml b/database/data/functors/empty_sets.yaml index b6cbaddf2..6a20120e7 100644 --- a/database/data/functors/empty_sets.yaml +++ b/database/data/functors/empty_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'Every category $\C$ has a unique functor $!_{\C} : \varnothing \to \C$. Here, we specify $\C = \Set$, but most of the properties do not depend on the choice of $\C$, as long as $\C$ is non-empty. This is the simplest example of a functor to $\Set$ that is both continuous and cocontinuous, but is neither representable nor a left or right adjoint.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/enveloping_group.yaml b/database/data/functors/enveloping_group.yaml index d0204fab2..260df85bd 100644 --- a/database/data/functors/enveloping_group.yaml +++ b/database/data/functors/enveloping_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: 'This functor maps a monoid $M$ to the group $F(M)$ that is equipped with a universal homomorphism $i_M : M \to F(M)$. It is called the (universal) enveloping group or the group completion of $M$; in the commutative case, it is known as the Grothendieck group of $M$. As a possible construction of $F(M)$, take the free group on generators $\underline{m}$ for $m \in M$ subject to the relations $\underline{1} = 1$ and $\underline{m \cdot n} = \underline{m} \cdot \underline{n}$.' nlab_link: https://ncatlab.org/nlab/show/free+functor left_adjoint: null +right_adjoint: forget_inverses tags: - algebra diff --git a/database/data/functors/forget_abelian.yaml b/database/data/functors/forget_abelian.yaml index b4d36e898..77c3f8c3d 100644 --- a/database/data/functors/forget_abelian.yaml +++ b/database/data/functors/forget_abelian.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps an abelian group to itself, considered merely as a group. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: abelianization +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_addition.yaml b/database/data/functors/forget_addition.yaml index a954e4a82..778b44d9a 100644 --- a/database/data/functors/forget_addition.yaml +++ b/database/data/functors/forget_addition.yaml @@ -6,6 +6,7 @@ codomain: Mon description: This functor maps a ring to its underlying multiplicative monoid, which as "forgotten" the addition of the ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: monoid_ring +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_commutative.yaml b/database/data/functors/forget_commutative.yaml index 0e50c8b45..fe2a22415 100644 --- a/database/data/functors/forget_commutative.yaml +++ b/database/data/functors/forget_commutative.yaml @@ -6,6 +6,7 @@ codomain: Ring description: This is the inclusion functor $\CRing \hookrightarrow \Ring$ that maps a commutative ring to itself, regarded merely as a ring. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # TODO: add the left adjoint to the database +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite.yaml b/database/data/functors/forget_finite.yaml index 9996e27cc..cd6f87e34 100644 --- a/database/data/functors/forget_finite.yaml +++ b/database/data/functors/forget_finite.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor is the inclusion functor $\FinSet \hookrightarrow \Set$ mapping a finite set to itself. It can also be regarded as a forgetful functor since it makes finite sets "forget" their finiteness. The functor is a basic example of a representable functor which is not a right adjoint. nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/forget_finite_abelian_group.yaml b/database/data/functors/forget_finite_abelian_group.yaml index 4afaac996..649147eb1 100644 --- a/database/data/functors/forget_finite_abelian_group.yaml +++ b/database/data/functors/forget_finite_abelian_group.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\FinAb \hookrightarrow \Ab$ that maps a finite abelian group to itself, regarded as an abelian group that has "forgotten" that it is finite. It provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_finite_group.yaml b/database/data/functors/forget_finite_group.yaml index 0d87d5de4..55b235457 100644 --- a/database/data/functors/forget_finite_group.yaml +++ b/database/data/functors/forget_finite_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: 'This is the inclusion functor $\FinGrp \hookrightarrow \Grp$. It can also be viewed as a forgetful functor that forgets the property of being finite. Among other things, it provides an example of a fully faithful functor that is neither finitary nor cofinitary.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group.yaml b/database/data/functors/forget_group.yaml index e88b3777d..50fead21b 100644 --- a/database/data/functors/forget_group.yaml +++ b/database/data/functors/forget_group.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a group $G$ to its underlying set $U_{\Grp}(G)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: free_group +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_group_pointed.yaml b/database/data/functors/forget_group_pointed.yaml index 776ca0ebe..bb5141854 100644 --- a/database/data/functors/forget_group_pointed.yaml +++ b/database/data/functors/forget_group_pointed.yaml @@ -6,6 +6,7 @@ codomain: Set_* description: This functor maps a group $G$ to its underlying pointed set $U_{\Grp,\Set_*}(G)$, whose base point is the identity element of $G$. It is an example of an essentially surjective functor which is not right-invertible. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_hausdorff.yaml b/database/data/functors/forget_hausdorff.yaml index 5cd125196..a4b70c6cb 100644 --- a/database/data/functors/forget_hausdorff.yaml +++ b/database/data/functors/forget_hausdorff.yaml @@ -6,6 +6,7 @@ codomain: Top description: This is the inclusion functor $\Haus \hookrightarrow \Top$ that maps a Hausdorff space to itself. It can also be viewed as a forgetful functor, since Hausdorff spaces "forget" that they are Hausdorff. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # TODO: add the Hausdorff reflection functor +right_adjoint: null tags: - topology diff --git a/database/data/functors/forget_inverses.yaml b/database/data/functors/forget_inverses.yaml index be8d4a8ee..f25cfbc02 100644 --- a/database/data/functors/forget_inverses.yaml +++ b/database/data/functors/forget_inverses.yaml @@ -6,6 +6,7 @@ codomain: Mon description: This functor maps a group to its underlying monoid. We view groups as structured sets $(X,m,e,i)$ (consisting of a set, a multiplication, a neutral element, and an inverse operation), and monoids as structured sets $(X,m,e)$. This forgetful functor precisely maps $(X,m,e,i)$ to $(X,m,e)$. From this point of view, it does not merely forget a property; it forgets an operation. This perspective is useful in contexts where the inverse operation is no longer reducible to a property, for example, the forgetful functor from topological groups to topological monoids. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: enveloping_group +right_adjoint: group_units tags: - algebra diff --git a/database/data/functors/forget_ring.yaml b/database/data/functors/forget_ring.yaml index 36ac92478..5199e2b25 100644 --- a/database/data/functors/forget_ring.yaml +++ b/database/data/functors/forget_ring.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a ring $R$ to its underlying set $U_{\Ring}(R)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_topology.yaml b/database/data/functors/forget_topology.yaml index 3cd74fd04..d5e9eb59a 100644 --- a/database/data/functors/forget_topology.yaml +++ b/database/data/functors/forget_topology.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a topological space $X$ to its underlying set $U_{\Top}(X)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: discrete_topology +right_adjoint: indiscrete_topology tags: - topology diff --git a/database/data/functors/forget_torsion.yaml b/database/data/functors/forget_torsion.yaml index 1cc5bd192..adbcfa047 100644 --- a/database/data/functors/forget_torsion.yaml +++ b/database/data/functors/forget_torsion.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\TorsAb \hookrightarrow \Ab$. It can also be viewed as a forgetful functor that forgets the property of being torsion. It is a typical example of a fully faithful functor that preserves finite products but does not preserve infinite products.' nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null # we only have the torsion functor Ab -> Ab in the database, not Ab -> TorsAb +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_torsion_free.yaml b/database/data/functors/forget_torsion_free.yaml index 5c4a3e619..c52066873 100644 --- a/database/data/functors/forget_torsion_free.yaml +++ b/database/data/functors/forget_torsion_free.yaml @@ -6,6 +6,7 @@ codomain: Ab description: 'This is the inclusion functor $\TorsFreeAb \hookrightarrow \Ab$. It can also be seen as a forgetful functor which forgets the property of being torsion-free. The functor provides a typical example of a fully faithful functor that does not preserve coequalizers and does not preserve epimorphisms.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/forget_vector.yaml b/database/data/functors/forget_vector.yaml index bfa2df0ff..6923a81d9 100644 --- a/database/data/functors/forget_vector.yaml +++ b/database/data/functors/forget_vector.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a vector space $V$ (over a fixed field $K$) to its underlying set $U_{\Vect}(V)$. nlab_link: https://ncatlab.org/nlab/show/forgetful+functor left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/free_group.yaml b/database/data/functors/free_group.yaml index 89d47b9a8..d08c7edba 100644 --- a/database/data/functors/free_group.yaml +++ b/database/data/functors/free_group.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps a set $X$ to the free group $F_{\Grp}(X)$ on that set. In the proofs, we abbreviate $F \coloneqq F_{\Grp}$. nlab_link: https://ncatlab.org/nlab/show/free+functor left_adjoint: null +right_adjoint: forget_group tags: - algebra diff --git a/database/data/functors/group_units.yaml b/database/data/functors/group_units.yaml index ad6f6312b..b8329db92 100644 --- a/database/data/functors/group_units.yaml +++ b/database/data/functors/group_units.yaml @@ -6,6 +6,7 @@ codomain: Grp description: This functor maps a monoid $M$ to its group of units $M^{\times}$, consisting of pairs $(a,b) \in M^2$ satisfying $ab=ba=1$. Equivalently, it takes the submonoid of invertible elements of $M$, equipped with the inverse operation. nlab_link: https://ncatlab.org/nlab/show/group+of+units left_adjoint: forget_inverses +right_adjoint: null tags: - algebra diff --git a/database/data/functors/id_Set.yaml b/database/data/functors/id_Set.yaml index 607ae5945..fd8a13b72 100644 --- a/database/data/functors/id_Set.yaml +++ b/database/data/functors/id_Set.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'Every category $\C$ has an identity functor $\id_{\C} : \C \to \C$. Here, we specify that $\C$ is the category of sets.' nlab_link: https://ncatlab.org/nlab/show/identity+functor left_adjoint: id_Set +right_adjoint: id_Set tags: - set theory diff --git a/database/data/functors/inclusion_ordinals.yaml b/database/data/functors/inclusion_ordinals.yaml index 2e7c98554..3c7d64990 100644 --- a/database/data/functors/inclusion_ordinals.yaml +++ b/database/data/functors/inclusion_ordinals.yaml @@ -6,6 +6,7 @@ codomain: On description: 'This is the inclusion map from the partially ordered set $(\IN \cup \{\infty\},\leq)$ (considered as a thin category as usual) into the partially ordered collection $(\On,\leq)$, where we map $\infty$ to the ordinal $\omega$. It is an example of a functor that preserves binary products, but not terminal objects.' nlab_link: https://ncatlab.org/nlab/show/identity+functor left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/indiscrete_topology.yaml b/database/data/functors/indiscrete_topology.yaml index 31593840f..ebda9939b 100644 --- a/database/data/functors/indiscrete_topology.yaml +++ b/database/data/functors/indiscrete_topology.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a set $X$ to the indiscrete topological space $I(X) \coloneqq (X, \{\varnothing,X\})$ in which only the empty set and $X$ are open. nlab_link: https://ncatlab.org/nlab/show/discrete+and+indiscrete+topology left_adjoint: forget_topology +right_adjoint: null tags: - topology diff --git a/database/data/functors/modulo-p.yaml b/database/data/functors/modulo-p.yaml index 74b4bc9ef..7c6789a07 100644 --- a/database/data/functors/modulo-p.yaml +++ b/database/data/functors/modulo-p.yaml @@ -6,6 +6,7 @@ codomain: Ab description: This functor maps an abelian group $A$ to the quotient $T^p(A) \coloneqq A/pA$, where $p$ is a fixed prime number. This group can also be represented as $A \otimes \IZ/p$. nlab_link: null left_adjoint: null +right_adjoint: p-torsion tags: - algebra diff --git a/database/data/functors/monoid_ring.yaml b/database/data/functors/monoid_ring.yaml index 673b5ca35..c3f7a35e9 100644 --- a/database/data/functors/monoid_ring.yaml +++ b/database/data/functors/monoid_ring.yaml @@ -6,6 +6,7 @@ codomain: Ring description: This functor maps a monoid $M$ to the monoid ring $\IZ[M]$, which consists of finite sums of elements in $M$. nlab_link: https://ncatlab.org/nlab/show/group+algebra left_adjoint: null +right_adjoint: forget_addition tags: - algebra diff --git a/database/data/functors/morphism_endpoints_inclusion.yaml b/database/data/functors/morphism_endpoints_inclusion.yaml index 6bb78f1d0..0de43353f 100644 --- a/database/data/functors/morphism_endpoints_inclusion.yaml +++ b/database/data/functors/morphism_endpoints_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_morphism description: This is the functor that embeds the discrete category $\{0,1\}$ into the walking morphism $\{0 \to 1\}$. It provides an example of a faithful functor that is full on isomorphisms but not full. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/nerve.yaml b/database/data/functors/nerve.yaml index c827c6736..9c13396d0 100644 --- a/database/data/functors/nerve.yaml +++ b/database/data/functors/nerve.yaml @@ -6,6 +6,7 @@ codomain: sSet description: The nerve of a small category $\C$ is the simplicial set $N(\C)$ whose $n$-simplices are chains of morphisms $X_0 \to \cdots \to X_n$. Among other things, it provides an example of a fully faithful functor that does not preserve regular epimorphisms. nlab_link: https://ncatlab.org/nlab/show/nerve left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/opposite_category.yaml b/database/data/functors/opposite_category.yaml index 6532ff0da..508c338f0 100644 --- a/database/data/functors/opposite_category.yaml +++ b/database/data/functors/opposite_category.yaml @@ -6,6 +6,7 @@ codomain: Cat description: 'This functor maps a small category $\C$ to its opposite category $\C^{\op}$ and a functor $F : \C \to \D$ to the opposite functor $F^{\op} : \C^{\op} \to \D^{\op}$.' nlab_link: https://ncatlab.org/nlab/show/opposite+category left_adjoint: opposite_category +right_adjoint: opposite_category tags: - category theory diff --git a/database/data/functors/opposite_monoid.yaml b/database/data/functors/opposite_monoid.yaml index d9837087d..5b0ca1360 100644 --- a/database/data/functors/opposite_monoid.yaml +++ b/database/data/functors/opposite_monoid.yaml @@ -6,6 +6,7 @@ codomain: Mon description: 'This functor maps a monoid $M$ to its opposite monoid $M^{\op}$ which has the multiplication $a *^{\op} b \coloneqq a * b$. A monoid homomorphism $f : M \to N$ is also a monoid homomorphism $f^{\op} : M^{\op} \to N^{\op}$.' nlab_link: https://ncatlab.org/nlab/show/opposite+magma left_adjoint: opposite_monoid +right_adjoint: opposite_monoid tags: - algebra diff --git a/database/data/functors/p-torsion.yaml b/database/data/functors/p-torsion.yaml index 26a4c043d..00e54523f 100644 --- a/database/data/functors/p-torsion.yaml +++ b/database/data/functors/p-torsion.yaml @@ -9,6 +9,7 @@ description: >- where $p$ is a fixed prime number. This group can also be represented as $\HomInternal(\IZ/p,A)$. nlab_link: null left_adjoint: modulo-p +right_adjoint: null tags: - algebra diff --git a/database/data/functors/pi_0.yaml b/database/data/functors/pi_0.yaml index 32fa83bea..509a2aa18 100644 --- a/database/data/functors/pi_0.yaml +++ b/database/data/functors/pi_0.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a topological space $X$ to its set $\pi_0(X)$ of path components. Thus, $\pi_0(X) = U(X) / {\sim}$, where $U(X)$ is the underlying set and $x \sim y$ when there is a path from $x$ to $y$. nlab_link: https://ncatlab.org/nlab/show/connected+space left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/pi_1.yaml b/database/data/functors/pi_1.yaml index b5295d99b..33768be6b 100644 --- a/database/data/functors/pi_1.yaml +++ b/database/data/functors/pi_1.yaml @@ -6,6 +6,7 @@ codomain: Grp description: The fundamental group $\pi_1(X,x_0)$ of a pointed topological space $(X,x_0)$ is the group of homotopy classes of loops at $x_0$. The group operation is concatenation of paths. For example, we have $\pi_1(S^1,1) \cong \IZ$ (see Hatcher's Algebraic Topology, Theorem 1.7). nlab_link: https://ncatlab.org/nlab/show/fundamental+group left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/power_set_contravariant.yaml b/database/data/functors/power_set_contravariant.yaml index 4a020b963..f0f6599d8 100644 --- a/database/data/functors/power_set_contravariant.yaml +++ b/database/data/functors/power_set_contravariant.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'This functor $P_{\forall}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced preimage operator $f^* : P(Y) \to P(X)$.' nlab_link: https://ncatlab.org/nlab/show/power+set left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/power_set_covariant.yaml b/database/data/functors/power_set_covariant.yaml index 1533afd21..31f11461e 100644 --- a/database/data/functors/power_set_covariant.yaml +++ b/database/data/functors/power_set_covariant.yaml @@ -6,6 +6,7 @@ codomain: Set description: 'This functor $P_{\exists}$ maps a set $X$ to its power set $P(X)$ and a map of sets $f : X \to Y$ to the induced image operator $f_* : P(X) \to P(Y)$.' nlab_link: https://ncatlab.org/nlab/show/power+set left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/rational_product.yaml b/database/data/functors/rational_product.yaml index 9be781954..a0ab1bea9 100644 --- a/database/data/functors/rational_product.yaml +++ b/database/data/functors/rational_product.yaml @@ -6,6 +6,7 @@ codomain: Top description: This functor maps a topological space $X$ to the topological space $X \times \IQ$, where $\IQ \subseteq \IR$ carries the usual topology. It is a typical example of a functor that preserves epimorphisms but not regular epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/ring_idempotents.yaml b/database/data/functors/ring_idempotents.yaml index 510453c04..cd7bb6f68 100644 --- a/database/data/functors/ring_idempotents.yaml +++ b/database/data/functors/ring_idempotents.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor sends a ring $R$ to its set $\Id(R)$ of idempotent elements. A ring homomorphism $R \to S$ restricts to a map $\Id(R) \to \Id(S)$. Among other things, it provides an example of a representable functor that does not preserve regular epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/sequences_sets.yaml b/database/data/functors/sequences_sets.yaml index ea1427914..ec7363fdb 100644 --- a/database/data/functors/sequences_sets.yaml +++ b/database/data/functors/sequences_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to the countable power $X^{\IN}$, i.e. the set of sequences in $X$. It is an example of a polynomial functor. It is also an example of a monadic functor for which the crude monadicity theorem does not apply. nlab_link: null left_adjoint: countable_copower_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/simple_group_probing.yaml b/database/data/functors/simple_group_probing.yaml index 1643e8cb8..60edf66e0 100644 --- a/database/data/functors/simple_group_probing.yaml +++ b/database/data/functors/simple_group_probing.yaml @@ -12,6 +12,7 @@ description: >- This is the canonical example of a continuous functor $\Grp \to \Set$ that is not representable, and not a right adjoint. nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/span_endpoints_inclusion.yaml b/database/data/functors/span_endpoints_inclusion.yaml index f4ad455e7..6a82fd1a7 100644 --- a/database/data/functors/span_endpoints_inclusion.yaml +++ b/database/data/functors/span_endpoints_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_span description: This is the functor that embeds the discrete category $\{1,2\}$ into the walking span $\{1 \leftarrow 0 \rightarrow 2\}$. Among other things, it provides an example of a fully faithful functor which is not left-invertible. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/squaring_sets.yaml b/database/data/functors/squaring_sets.yaml index e95e558a9..59b1a4898 100644 --- a/database/data/functors/squaring_sets.yaml +++ b/database/data/functors/squaring_sets.yaml @@ -6,6 +6,7 @@ codomain: Set description: This functor maps a set $X$ to its square $X^2$. It is a simple example of a polynomial functor. nlab_link: null left_adjoint: doubling_sets +right_adjoint: null tags: - set theory diff --git a/database/data/functors/stone-cech-compactification.yaml b/database/data/functors/stone-cech-compactification.yaml index 165f1443b..9b43842e2 100644 --- a/database/data/functors/stone-cech-compactification.yaml +++ b/database/data/functors/stone-cech-compactification.yaml @@ -9,6 +9,7 @@ description: >- Among other things, this functor provides an example of a reflector that does not preserve binary products. nlab_link: https://ncatlab.org/nlab/show/Stone-%C4%8Cech+compactification left_adjoint: null +right_adjoint: null tags: - topology diff --git a/database/data/functors/torsion.yaml b/database/data/functors/torsion.yaml index 50f0778ba..3fab4b8fe 100644 --- a/database/data/functors/torsion.yaml +++ b/database/data/functors/torsion.yaml @@ -8,6 +8,7 @@ description: >- $$T(A) \coloneqq \{a \in A : \exists n \geq 1 \, (na = 0)\}.$$ nlab_link: https://ncatlab.org/nlab/show/torsion+subgroup left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_BG.yaml b/database/data/functors/trivial_BG.yaml index 205035760..51582aed3 100644 --- a/database/data/functors/trivial_BG.yaml +++ b/database/data/functors/trivial_BG.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the delooping of a non-trivial group $G$. It is a basic example of a conservative functor which is not faithful.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_Idem.yaml b/database/data/functors/trivial_Idem.yaml index af27dd9bc..1c31eb27b 100644 --- a/database/data/functors/trivial_Idem.yaml +++ b/database/data/functors/trivial_Idem.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the walking idempotent. It is a basic example of an essentially injective functor which is not conservative.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/trivial_groups.yaml b/database/data/functors/trivial_groups.yaml index 112e6d358..0d40eb32a 100644 --- a/database/data/functors/trivial_groups.yaml +++ b/database/data/functors/trivial_groups.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of groups. It is a basic example of a full functor which is not faithful.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - algebra diff --git a/database/data/functors/trivial_sets.yaml b/database/data/functors/trivial_sets.yaml index aaa860557..86e3226d1 100644 --- a/database/data/functors/trivial_sets.yaml +++ b/database/data/functors/trivial_sets.yaml @@ -6,6 +6,7 @@ codomain: '1' description: 'Every category $\C$ has a unique functor $!_{\C} : \C \to 1$ into the trivial category. Here, we specify that $\C$ is the category of sets.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - set theory diff --git a/database/data/functors/walking_isomorphism_object_inclusion.yaml b/database/data/functors/walking_isomorphism_object_inclusion.yaml index 8955508cb..2a504dbd1 100644 --- a/database/data/functors/walking_isomorphism_object_inclusion.yaml +++ b/database/data/functors/walking_isomorphism_object_inclusion.yaml @@ -6,6 +6,7 @@ codomain: walking_isomorphism description: 'This is the natural embedding of the trivial category with a single object $0$ into the walking isomorphism given by two objects $0,1$ and an isomorphism $0 \to 1$. This is the simplest example of an equivalence of categories which is not an isomorphism.' nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/functors/walking_morphism_representation.yaml b/database/data/functors/walking_morphism_representation.yaml index 0a7acf257..2691d2b36 100644 --- a/database/data/functors/walking_morphism_representation.yaml +++ b/database/data/functors/walking_morphism_representation.yaml @@ -6,6 +6,7 @@ codomain: Set description: This is the functor $I \to \Set$ that maps the universal morphism $0 \to 1$ to the unique map $\varnothing \to \{*\}$ in $\Set$. It provides a very simple example of a functor that preserves coequalizers (and hence regular epimorphisms) but does not preserve epimorphisms. nlab_link: null left_adjoint: null +right_adjoint: null tags: - category theory diff --git a/database/data/morphism-implications/misc.yaml b/database/data/morphism-implications/misc.yaml index b5e4e52e7..6dd219795 100644 --- a/database/data/morphism-implications/misc.yaml +++ b/database/data/morphism-implications/misc.yaml @@ -1,6 +1,6 @@ - id: thin_implies_constant assumptions: [] - mapped_assumptions: + associated_assumptions: category: - thin conclusions: @@ -20,7 +20,7 @@ - id: zero_morphism_criterion assumptions: - constant - mapped_assumptions: + associated_assumptions: category: - zero morphisms conclusions: diff --git a/database/data/morphism-implications/mono-epi-iso.yaml b/database/data/morphism-implications/mono-epi-iso.yaml index fdd418f3f..040be5a18 100644 --- a/database/data/morphism-implications/mono-epi-iso.yaml +++ b/database/data/morphism-implications/mono-epi-iso.yaml @@ -29,7 +29,7 @@ - id: mono_is_iso assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - subobject-trivial conclusions: @@ -41,7 +41,7 @@ assumptions: - monomorphism - epimorphism - mapped_assumptions: + associated_assumptions: category: - balanced conclusions: @@ -52,7 +52,7 @@ - id: mono-regular_def assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - mono-regular conclusions: @@ -79,7 +79,7 @@ - id: strict_monos_are_often_effective assumptions: - strict monomorphism - mapped_assumptions: + associated_assumptions: category: - pushouts conclusions: @@ -95,7 +95,7 @@ - id: iso_is_normal_mono assumptions: - isomorphism - mapped_assumptions: + associated_assumptions: category: - zero morphisms conclusions: @@ -114,7 +114,7 @@ - id: regular_implies_normal_mono_preadditive_case assumptions: - regular monomorphism - mapped_assumptions: + associated_assumptions: category: - preadditive conclusions: @@ -164,7 +164,7 @@ - id: extremal_monos_are_regular_in_coregular_category assumptions: - extremal monomorphism - mapped_assumptions: + associated_assumptions: category: - coregular conclusions: @@ -178,7 +178,7 @@ - id: extremal_mono_strong_criterion assumptions: - extremal monomorphism - mapped_assumptions: + associated_assumptions: category: - pushouts conclusions: @@ -195,7 +195,7 @@ - id: extremal_mono_balanced assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - balanced conclusions: @@ -206,7 +206,7 @@ - id: every_mono_strong_criterion assumptions: - monomorphism - mapped_assumptions: + associated_assumptions: category: - epi-regular conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/closed.yaml b/database/data/symmetric_monoidal_category_implications/closed.yaml index 1b83ed28d..5da42f186 100644 --- a/database/data/symmetric_monoidal_category_implications/closed.yaml +++ b/database/data/symmetric_monoidal_category_implications/closed.yaml @@ -3,7 +3,7 @@ - id: closed_cartesian_symmetric_monoidal assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - cartesian closed conclusions: @@ -14,7 +14,7 @@ - id: when_closed_implies_cocomplete assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - cocomplete conclusions: @@ -25,7 +25,7 @@ - id: when_closed_implies_finitely_cocomplete assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - finitely cocomplete conclusions: @@ -36,7 +36,7 @@ - id: when_closed_implies_distributive assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - finite coproducts conclusions: @@ -47,7 +47,7 @@ - id: when_closed_implies_infinitary_distributive assumptions: - closed - mapped_assumptions: + associated_assumptions: underlying_category: - coproducts conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml index 02a7f4167..de4941f54 100644 --- a/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml +++ b/database/data/symmetric_monoidal_category_implications/limits-colimits.yaml @@ -28,7 +28,7 @@ - id: distributive_cartesian assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - distributive conclusions: @@ -40,7 +40,7 @@ - id: infinitary_distributive_cartesian assumptions: - cartesian - mapped_assumptions: + associated_assumptions: underlying_category: - infinitary distributive conclusions: @@ -61,7 +61,7 @@ - id: preadditive_codistributive_criterion assumptions: - distributive - mapped_assumptions: + associated_assumptions: underlying_category: - biproducts conclusions: diff --git a/database/data/symmetric_monoidal_category_implications/misc.yaml b/database/data/symmetric_monoidal_category_implications/misc.yaml index 26f25512a..e1fdfc0ff 100644 --- a/database/data/symmetric_monoidal_category_implications/misc.yaml +++ b/database/data/symmetric_monoidal_category_implications/misc.yaml @@ -22,7 +22,7 @@ - id: thin_is_well_pointed assumptions: [] - mapped_assumptions: + associated_assumptions: underlying_category: - thin conclusions: diff --git a/database/schema/001_structures.sql b/database/schema/001_structures.sql index cf73970a7..4df33d6ad 100644 --- a/database/schema/001_structures.sql +++ b/database/schema/001_structures.sql @@ -9,23 +9,27 @@ INSERT INTO structure_types (type) VALUES ('symmetric_monoidal_category'); -CREATE TABLE structure_maps ( - map TEXT NOT NULL, +CREATE TABLE associated_structure_types ( + label TEXT NOT NULL, type TEXT NOT NULL, - mapped_type TEXT NOT NULL, - PRIMARY KEY (map, type, mapped_type), - UNIQUE (map, type), + associated_type TEXT NOT NULL, + required INTEGER NOT NULL + CHECK (required in (TRUE, FALSE)), + PRIMARY KEY (label, type, associated_type), + UNIQUE (label, type), FOREIGN KEY (type) REFERENCES structure_types (type) ON DELETE CASCADE, - FOREIGN KEY (mapped_type) REFERENCES structure_types (type) ON DELETE CASCADE + FOREIGN KEY (associated_type) REFERENCES structure_types (type) ON DELETE CASCADE ); -INSERT INTO structure_maps - (map, type, mapped_type) +INSERT INTO associated_structure_types + (label, type, associated_type, required) VALUES - ('domain', 'functor', 'category'), - ('codomain', 'functor', 'category'), - ('category', 'morphism', 'category'), - ('underlying_category', 'symmetric_monoidal_category', 'category'); + ('domain', 'functor', 'category', TRUE), + ('codomain', 'functor', 'category', TRUE), + ('category', 'morphism', 'category', TRUE), + ('underlying_category', 'symmetric_monoidal_category', 'category', TRUE), + ('left_adjoint', 'functor', 'functor', FALSE), + ('right_adjoint', 'functor', 'functor', FALSE); CREATE TABLE structures ( id TEXT PRIMARY KEY, @@ -80,4 +84,19 @@ 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 associated_structures ( + label TEXT NOT NULL, + type TEXT NOT NULL, + associated_type TEXT NOT NULL, + structure_id TEXT NOT NULL, + associated_structure_id TEXT NOT NULL, + FOREIGN KEY (label, type, associated_type) + REFERENCES associated_structure_types (label, type, associated_type) + ON DELETE CASCADE, + FOREIGN KEY (structure_id, type) + REFERENCES structures (id, type) ON DELETE CASCADE, + FOREIGN KEY (associated_structure_id, associated_type) + REFERENCES structures (id, type) ON DELETE CASCADE ); \ No newline at end of file diff --git a/database/schema/003_implications.sql b/database/schema/003_implications.sql index 0d3738df7..a9c94bd22 100644 --- a/database/schema/003_implications.sql +++ b/database/schema/003_implications.sql @@ -38,23 +38,23 @@ CREATE TABLE conclusions ( CREATE INDEX idx_conclusions_property ON conclusions (property_id); -CREATE TABLE mapped_assumptions ( +CREATE TABLE associated_assumptions ( implication_id TEXT NOT NULL, - map TEXT NOT NULL, + label TEXT NOT NULL, property_id TEXT NOT NULL, type TEXT NOT NULL, property_type TEXT NOT NULL, - PRIMARY KEY (implication_id, map, property_id), + PRIMARY KEY (implication_id, label, property_id), FOREIGN KEY (implication_id, type) REFERENCES implications (id, type) ON DELETE CASCADE, FOREIGN KEY (property_id, property_type) REFERENCES properties (id, type) ON DELETE CASCADE, - FOREIGN KEY (map, type, property_type) - REFERENCES structure_maps (map, type, mapped_type) + FOREIGN KEY (label, type, property_type) + REFERENCES associated_structure_types (label, type, associated_type) ON DELETE RESTRICT ); -CREATE INDEX idx_assumptions_mapped_property ON mapped_assumptions (property_id); +CREATE INDEX idx_assumptions_associated_property ON associated_assumptions (property_id); CREATE VIEW implications_view AS SELECT @@ -74,15 +74,15 @@ CREATE VIEW implications_view AS ORDER BY lower(c.property_id) ) AS conclusions, ( - SELECT json_group_object(map, properties) + SELECT json_group_object(label, properties) FROM ( SELECT - a.map, + a.label, json_group_array(a.property_id) AS properties - FROM mapped_assumptions a + FROM associated_assumptions a WHERE a.implication_id = i.id - GROUP BY a.map + GROUP BY a.label ) - ) AS mapped_assumptions + ) AS associated_assumptions FROM implications i ; \ No newline at end of file diff --git a/database/schema/007_functors.sql b/database/schema/007_functors.sql deleted file mode 100644 index 982d01210..000000000 --- a/database/schema/007_functors.sql +++ /dev/null @@ -1,24 +0,0 @@ -CREATE TABLE functors ( - id TEXT PRIMARY KEY, - domain TEXT NOT NULL, - codomain TEXT NOT NULL, - left_adjoint TEXT, - UNIQUE (id, domain, codomain), - FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (domain) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (codomain) REFERENCES categories (id) ON DELETE CASCADE, - FOREIGN KEY (left_adjoint, codomain, domain) - REFERENCES functors (id, domain, codomain) - ON DELETE CASCADE -); - -CREATE TRIGGER trg_functor_type_check -BEFORE INSERT ON functors -BEGIN - SELECT - CASE - WHEN - (SELECT type FROM structures WHERE id = NEW.id) != 'functor' - THEN RAISE(ABORT, 'Functors must have type "functor"') - END; -END; \ No newline at end of file diff --git a/database/schema/008_morphisms.sql b/database/schema/008_morphisms.sql deleted file mode 100644 index dfc9ea414..000000000 --- a/database/schema/008_morphisms.sql +++ /dev/null @@ -1,17 +0,0 @@ -CREATE TABLE morphisms ( - id TEXT PRIMARY KEY, - category TEXT NOT NULL, - FOREIGN KEY (id) REFERENCES structures (id) ON DELETE CASCADE, - FOREIGN KEY (category) REFERENCES categories (id) ON DELETE CASCADE -); - -CREATE TRIGGER trg_morphism_type_check -BEFORE INSERT ON morphisms -BEGIN - SELECT - CASE - WHEN - (SELECT type FROM structures WHERE id = NEW.id) != 'morphism' - THEN RAISE(ABORT, 'Morphisms must have type "morphism"') - END; -END; \ No newline at end of file diff --git a/database/schema/009_symmetric-monoidal-categories.sql b/database/schema/009_symmetric-monoidal-categories.sql deleted file mode 100644 index b9ceab78e..000000000 --- a/database/schema/009_symmetric-monoidal-categories.sql +++ /dev/null @@ -1,17 +0,0 @@ -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 6eafa4966..b72bb540f 100644 --- a/database/scripts/deduce-implications.ts +++ b/database/scripts/deduce-implications.ts @@ -24,10 +24,10 @@ export function clear_deduced_implications(type: StructureType) { * then P^op ===> Q^op holds as well. */ export function create_dualized_implications(type: StructureType) { - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps WHERE type = ?` + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) @@ -40,7 +40,7 @@ export function create_dualized_implications(type: StructureType) { conclusions: string dual_assumptions: string dual_conclusions: string - dual_mapped_assumptions: string + dual_associated_assumptions: string } >( `SELECT @@ -63,18 +63,18 @@ export function create_dualized_implications(type: StructureType) { WHERE a.implication_id = i.id ) AS dual_conclusions, ( - SELECT json_group_object(map, properties) + SELECT json_group_object(label, properties) FROM ( SELECT - a.map, + a.label, json_group_array(p.dual_property_id) AS properties - FROM mapped_assumptions a + FROM associated_assumptions a INNER JOIN properties p ON p.id = a.property_id AND p.type = a.property_type WHERE a.implication_id = i.id - GROUP BY a.map + GROUP BY a.label ) - ) AS dual_mapped_assumptions + ) AS dual_associated_assumptions FROM implications_view i WHERE i.type = ? AND i.is_deduced = FALSE` ) @@ -97,9 +97,9 @@ export function create_dualized_implications(type: StructureType) { VALUES (?, ?, ?) `) - const mapped_assumption_insert = db.prepare(` - INSERT INTO mapped_assumptions - (implication_id, map, property_id, type, property_type) + const associated_assumption_insert = db.prepare(` + INSERT INTO associated_assumptions + (implication_id, label, property_id, type, property_type) VALUES (?, ?, ?, ?, ?) `) @@ -113,14 +113,16 @@ export function create_dualized_implications(type: StructureType) { const dual_assumptions = parse_json_set(impl.dual_assumptions) const conclusions = parse_json_set(impl.conclusions) const dual_conclusions = parse_json_set(impl.dual_conclusions) - const dual_mapped_assumptions = parse_nested_json_set( - impl.dual_mapped_assumptions + const dual_associated_assumptions = parse_nested_json_set( + impl.dual_associated_assumptions ) if (dual_assumptions.has(null)) continue if (dual_conclusions.has(null)) continue - if (Object.values(dual_mapped_assumptions).some((set) => set?.has(null))) { + if ( + Object.values(dual_associated_assumptions).some((set) => set?.has(null)) + ) { continue } @@ -148,10 +150,16 @@ export function create_dualized_implications(type: StructureType) { conclusion_insert.run(dual_id, c, type) } - for (const { map, mapped_type } of structure_maps) { - const duals = dual_mapped_assumptions[map] + for (const { label, associated_type } of associated_structure_types) { + const duals = dual_associated_assumptions[label] for (const d of duals ?? []) { - mapped_assumption_insert.run(dual_id, map, d, type, mapped_type) + associated_assumption_insert.run( + dual_id, + label, + d, + type, + associated_type + ) } } } diff --git a/database/scripts/restrict-functor-properties.ts b/database/scripts/restrict-functor-properties.ts index 0fd26e37b..7230b0092 100644 --- a/database/scripts/restrict-functor-properties.ts +++ b/database/scripts/restrict-functor-properties.ts @@ -29,15 +29,18 @@ function restrict_representable_functors() { check_redundancy ) SELECT - f.id, + a.structure_id, 'representable', 'functor', FALSE, 'The codomain is not $\\Set$.', TRUE, FALSE - FROM functors f - WHERE f.codomain <> 'Set' + FROM associated_structures a + WHERE + a.type = 'functor' + AND a.label = 'codomain' + AND a.associated_structure_id <> 'Set' ON CONFLICT (structure_id, property_id) DO UPDATE SET proof = excluded.proof, diff --git a/database/scripts/restrict-morphism-properties.ts b/database/scripts/restrict-morphism-properties.ts index cdde6fdc9..e9e087f96 100644 --- a/database/scripts/restrict-morphism-properties.ts +++ b/database/scripts/restrict-morphism-properties.ts @@ -6,6 +6,7 @@ const db = get_client({ readonly: false }) /** * Ensures that certain properties of morphisms are only satisfied * when the ambient categories have certain properties. + * TODO: rework this once we have category_conclusions */ export function restrict_morphism_properties() { restrict_normal_morphisms('mono') @@ -31,21 +32,23 @@ function restrict_normal_morphisms(variant: 'mono' | 'epi') { check_redundancy ) SELECT - m.id, + sa.structure_id, ?, 'morphism', FALSE, 'The ' || c.name || ' has no zero morphisms.', TRUE, FALSE - FROM morphisms m + FROM associated_structures sa + INNER JOIN structures c + ON c.id = sa.associated_structure_id INNER JOIN property_assignments a - ON a.structure_id = m.category - INNER JOIN structures c - ON c.id = m.category - WHERE a.type = 'category' - AND a.property_id = 'zero morphisms' - AND a.is_satisfied = FALSE + ON a.structure_id = c.id + WHERE + sa.type = 'morphism' + AND sa.label = 'category' + AND a.property_id = 'zero morphisms' + AND a.is_satisfied = FALSE ON CONFLICT (structure_id, property_id) DO UPDATE SET proof = excluded.proof, diff --git a/database/scripts/seed.ts b/database/scripts/seed.ts index f475f8347..9d08286fb 100644 --- a/database/scripts/seed.ts +++ b/database/scripts/seed.ts @@ -5,16 +5,13 @@ import type { CategoryYaml, ConfigYaml, ImplicationYaml, - FunctorYaml, SpecialMorphismRuleYaml, StructureYaml, - PropertyYaml, - MorphismYaml, - SymmetricMonoidalCategoryYaml + PropertyYaml } from './utils/seed.types' import { create_schema_hash, get_saved_schema_hash } from './utils/schema' import { STRUCTURE_TYPES, type StructureType, PLURALS } from '$shared/config' -import { are_disjoint, devlog } from '$shared/utils' +import { are_disjoint, capitalize, devlog } from '$shared/utils' const db = get_client({ readonly: false }) @@ -39,11 +36,11 @@ function seed() { seed_properties({ type: 'functor', folder: 'functor-properties' }) seed_implications({ type: 'functor', folder: 'functor-implications' }) - seed_structures({ type: 'functor', folder: 'functors', extra: insert_functor }) + seed_structures({ type: 'functor', folder: 'functors' }) seed_properties({ type: 'morphism', folder: 'morphism-properties' }) seed_implications({ type: 'morphism', folder: 'morphism-implications' }) - seed_structures({ type: 'morphism', folder: 'morphisms', extra: insert_morphism }) + seed_structures({ type: 'morphism', folder: 'morphisms' }) seed_properties({ type: 'symmetric_monoidal_category', @@ -55,8 +52,7 @@ function seed() { }) seed_structures({ type: 'symmetric_monoidal_category', - folder: 'symmetric_monoidal_categories', - extra: insert_symmetric_monoidal_category + folder: 'symmetric_monoidal_categories' }) } @@ -90,7 +86,7 @@ function clear_all_tables() { db.prepare(`DELETE FROM special_object_assignments`).run() db.prepare(`DELETE FROM special_object_types`).run() - db.prepare(`DELETE FROM mapped_assumptions`).run() + db.prepare(`DELETE FROM associated_assumptions`).run() db.prepare(`DELETE FROM assumptions`).run() db.prepare(`DELETE FROM conclusions`).run() db.prepare(`DELETE FROM implications`).run() @@ -108,6 +104,7 @@ function clear_all_tables() { db.prepare(`DELETE FROM relations`).run() db.prepare(`DELETE FROM structures`).run() + db.prepare(`DELETE FROM associated_structures`).run() }) try { @@ -210,6 +207,16 @@ function seed_structures({ folder: string extra?: (structure: T) => void }) { + const associated_structure_types = db + .prepare< + [StructureType], + { label: keyof T; associated_type: StructureType; required: 0 | 1 } + >( + `SELECT label, associated_type, required + FROM associated_structure_types WHERE type = ?` + ) + .all(type) + const structure_insert = db.prepare( `INSERT INTO structures ( id, type, name, notation, description, nlab_link, @@ -246,6 +253,13 @@ function seed_structures({ ) VALUES (?, ?, ?, ?)` ) + const associated_structure_insert = db.prepare( + `INSERT INTO associated_structures ( + label, type, associated_type, + structure_id, associated_structure_id + ) VALUES (?, ?, ?, ?, ?)` + ) + function insert_structure(structure: T) { const properties_are_disjoint = are_disjoint( [ @@ -272,8 +286,27 @@ function seed_structures({ structure.parent || null ) + for (const { label, associated_type, required } of associated_structure_types) { + if (required && !structure[label]) { + console.error( + `❌ ${capitalize(type)} "${structure.id}" has no ${label.toString()}` + ) + process.exit(1) + } + + if (structure[label]) { + associated_structure_insert.run( + label, + type, + associated_type, + structure.id, + structure[label] + ) + } + } + if (!structure.tags.length) { - console.error(`❌ Structure "${structure.id}" has no tags`) + console.error(`❌ ${capitalize(type)} "${structure.id}" has no tags`) process.exit(1) } @@ -346,36 +379,6 @@ function insert_category(category: CategoryYaml) { } } -/** - * Inserts the data of a functor that is specific to functors. - */ -function insert_functor(functor: FunctorYaml) { - db.prepare( - `INSERT INTO functors (id, domain, codomain, left_adjoint) - VALUES (?, ?, ?, ?)` - ).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) { - db.prepare( - `INSERT INTO morphisms (id, category) - VALUES (?, ?)` - ).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) -} - /** * Seeds all properties of a given type from YAML files. */ @@ -436,10 +439,10 @@ function seed_properties({ type, folder }: { type: StructureType; folder: string * Seeds all implications of a given type from YAML files. */ function seed_implications({ type, folder }: { type: StructureType; folder: string }) { - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps WHERE type = ?` + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) @@ -461,15 +464,15 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri ) VALUES (?, ?, ?)` ) - const mapped_assumption_insert = db.prepare( - `INSERT INTO mapped_assumptions ( - implication_id, map, property_id, type, property_type + const associated_assumption_insert = db.prepare( + `INSERT INTO associated_assumptions ( + implication_id, label, property_id, type, property_type ) VALUES (?, ?, ?, ?, ?)` ) function insert_implications(implications: ImplicationYaml[]) { for (const impl of implications) { - if (!impl.assumptions.length && !impl.mapped_assumptions) { + if (!impl.assumptions.length && !impl.associated_assumptions) { console.error(`❌ Implication ${impl.id} has no assumptions.`) process.exit(1) } @@ -489,12 +492,18 @@ function seed_implications({ type, folder }: { type: StructureType; folder: stri conclusion_insert.run(impl.id, conclusion, type) } - if (!impl.mapped_assumptions) continue + if (!impl.associated_assumptions) continue - for (const { map, mapped_type } of structure_maps) { - const assumptions = impl.mapped_assumptions[map] ?? [] + for (const { label, associated_type } of associated_structure_types) { + const assumptions = impl.associated_assumptions[label] ?? [] for (const p of assumptions) { - mapped_assumption_insert.run(impl.id, map, p, type, mapped_type) + associated_assumption_insert.run( + impl.id, + label, + p, + type, + associated_type + ) } } } diff --git a/database/scripts/test.ts b/database/scripts/test.ts index 76e6b5b02..79ef2c916 100644 --- a/database/scripts/test.ts +++ b/database/scripts/test.ts @@ -53,6 +53,7 @@ function execute_tests() { { forget_vector: forget_vector_expected }, 'functor' ) + test_adjoint_functor_relationships() devlog('\n--- Test morphisms ---') @@ -300,3 +301,120 @@ function check_link_targets_exist() { devlog(`✅ Link targets exist`) } + +/** + * Tests for functors that if L is left adjoint to R, + * then R is right adjoint to L, and vice versa. + * Also tests dom(L)=cod(R) and cod(L)=dom(R). + */ +function test_adjoint_functor_relationships() { + const checks: Array<{ + query: string + format: (row: Record) => string + }> = [ + { + query: ` + SELECT + sm1.structure_id AS right_1, + sm1.associated_structure_id AS left, + sm2.associated_structure_id AS right_2 + FROM associated_structures sm1 + LEFT JOIN associated_structures sm2 + ON + sm2.type = 'functor' + AND sm2.structure_id = sm1.associated_structure_id + AND sm2.label = 'right_adjoint' + WHERE + sm1.type = 'functor' + AND sm1.label = 'left_adjoint' + AND (right_2 IS NULL OR right_2 <> right_1) + `, + format: ({ right_1, left, right_2 }) => + `❌ Adjoint asymmetry: ${left} is declared as left adjoint to ${right_1}, but ${right_2 ?? 'no functor'} is recorded as its right adjoint.` + }, + { + query: ` + SELECT + sm1.structure_id AS left_1, + sm1.associated_structure_id AS right, + sm2.associated_structure_id AS left_2 + FROM associated_structures sm1 + LEFT JOIN associated_structures sm2 + ON + sm2.type = 'functor' + AND sm2.structure_id = sm1.associated_structure_id + AND sm2.label = 'left_adjoint' + WHERE + sm1.type = 'functor' + AND sm1.label = 'right_adjoint' + AND (left_2 IS NULL OR left_2 <> left_1) + `, + format: ({ left_1, right, left_2 }) => + `❌ Adjoint asymmetry: ${right} is declared as right adjoint to ${left_1}, but ${left_2 ?? 'no functor'} is recorded as its left adjoint.` + }, + { + query: ` + SELECT + sm.structure_id AS functor, + sm.associated_structure_id AS left_adjoint, + dom.associated_structure_id AS functor_domain, + adj_cod.associated_structure_id AS left_adjoint_codomain + FROM + associated_structures sm + INNER JOIN associated_structures dom + ON + dom.label = 'domain' + AND dom.type = 'functor' + AND dom.structure_id = sm.structure_id + INNER JOIN associated_structures adj_cod + ON + adj_cod.label = 'codomain' + AND adj_cod.type = 'functor' + AND adj_cod.structure_id = sm.associated_structure_id + WHERE + sm.label = 'left_adjoint' + AND functor_domain <> left_adjoint_codomain + `, + format: ({ functor, left_adjoint, functor_domain, left_adjoint_codomain }) => + `❌ Domain/codomain mismatch: ${functor} has domain ${functor_domain}, but its left adjoint ${left_adjoint} has codomain ${left_adjoint_codomain}.` + }, + { + query: ` + SELECT + sm.structure_id AS functor, + sm.associated_structure_id AS left_adjoint, + cod.associated_structure_id AS functor_codomain, + adj_dom.associated_structure_id AS left_adjoint_domain + FROM + associated_structures sm + INNER JOIN associated_structures cod + ON + cod.label = 'codomain' + AND cod.type = 'functor' + AND cod.structure_id = sm.structure_id + INNER JOIN associated_structures adj_dom + ON + adj_dom.label = 'domain' + AND adj_dom.type = 'functor' + AND adj_dom.structure_id = sm.associated_structure_id + WHERE + sm.label = 'left_adjoint' + AND functor_codomain <> left_adjoint_domain`, + format: ({ functor, left_adjoint, functor_codomain, left_adjoint_domain }) => + `❌ Domain/codomain mismatch: ${functor} has codomain ${functor_codomain}, but its left adjoint ${left_adjoint} has domain ${left_adjoint_domain}.` + } + ] + + const violations = checks.flatMap(({ query, format }) => + db + .prepare>(query) + .all() + .map((row) => format(row)) + ) + + if (violations.length > 0) { + throw new Error(violations.join('\n')) + } + + console.info('✅ Adjoint functor relationships are valid') +} diff --git a/database/scripts/utils/implications.ts b/database/scripts/utils/implications.ts index 90778783a..fd96cf1cd 100644 --- a/database/scripts/utils/implications.ts +++ b/database/scripts/utils/implications.ts @@ -21,16 +21,16 @@ function get_assumption_string( .join(' and ') : `is a ${remove_underscores(type)}` - if (!implication.mapped_assumptions) return own + if (!implication.associated_assumptions) return own - const mapped = Object.entries(implication.mapped_assumptions) + const associated = Object.entries(implication.associated_assumptions) .map( ([map, props]) => `and the ${remove_underscores(map)} has the required properties (${Array.from(props!).join(', ')})` ) .join(', ') - return `${own}, ${mapped}` + return `${own}, ${associated}` } function get_conclusion_string( @@ -71,7 +71,7 @@ export function get_contradiction_string( const conclusion_string = get_conclusion_string(implication, properties_dict, true) const has_multiple_assumptions = - implication.assumptions.size > 1 || !!implication.mapped_assumptions + implication.assumptions.size > 1 || !!implication.associated_assumptions const ref = `by this result` diff --git a/database/scripts/utils/seed.types.ts b/database/scripts/utils/seed.types.ts index dfc372d82..7009feb84 100644 --- a/database/scripts/utils/seed.types.ts +++ b/database/scripts/utils/seed.types.ts @@ -70,20 +70,6 @@ export type CategoryYaml = StructureYaml & { special_morphisms: Record } -export type FunctorYaml = StructureYaml & { - domain: string - codomain: string - left_adjoint: string | null -} - -export type MorphismYaml = StructureYaml & { - category: string -} - -export type SymmetricMonoidalCategoryYaml = StructureYaml & { - underlying_category: string -} - export type PropertyYaml = { id: string relation: string @@ -99,7 +85,7 @@ export type ImplicationYaml = { id: string assumptions: string[] conclusions: string[] - mapped_assumptions?: Partial> + associated_assumptions?: Partial> proof: string is_equivalence: boolean } diff --git a/database/scripts/utils/structures.ts b/database/scripts/utils/structures.ts index 88978aaba..c23735c18 100644 --- a/database/scripts/utils/structures.ts +++ b/database/scripts/utils/structures.ts @@ -11,67 +11,61 @@ export type StructureMeta = { associated_satisfied_properties?: Partial>> } -/** - * Dictionary associating to every structure type the name of the table. - */ -const TABLES: Record = { - category: 'categories', - functor: 'functors', - morphism: 'morphisms', - symmetric_monoidal_category: 'symmetric_monoidal_categories' -} - /** * Returns the list of stored categorical structures of a given type. * For structures with structure maps (e.g. functors), the associated * satisfied properties are retrieved as well. */ export function get_structures(db: Database, type: StructureType): StructureMeta[] { - const structures = db - .prepare<[StructureType], StructureMeta>( - `SELECT - s.id, - s.name, - s.dual_structure_id AS dual - FROM structures s - WHERE s.type = ? - ORDER BY lower(s.name)` - ) - .all(type) - - const structure_maps = db - .prepare<[StructureType], string>( - `SELECT map - FROM structure_maps - WHERE type = ?` + const structures_raw = db + .prepare< + [StructureType], + { + id: string + name: string + dual: string | null + properties: string + } + >( + `WITH associated_properties AS ( + SELECT + s.id, + s.name, + s.dual_structure_id AS dual, + m.label, + json_group_array(a.property_id) AS props + FROM structures s + LEFT JOIN associated_structures m + ON m.structure_id = s.id + LEFT JOIN property_assignments a + ON a.structure_id = m.associated_structure_id + AND a.is_satisfied = TRUE + WHERE s.type = ? + GROUP BY s.id, m.label + ) + SELECT + id, name, dual, + json_group_object(label, props) AS properties + FROM associated_properties + GROUP BY id + ORDER BY id` ) - .pluck() .all(type) - if (!structure_maps.length) return structures - - const add_associated_properties = db.transaction(() => { - for (const map of structure_maps) { - const prop_query = db - .prepare<[string], string>( - `SELECT property_id FROM property_assignments - INNER JOIN ${TABLES[type]} t ON t.id = ? - WHERE structure_id = t.${map} - AND is_satisfied = TRUE` - ) - .pluck() + return structures_raw.map((s) => { + const { id, name, dual, properties } = s + const parsed_properties = JSON.parse(properties) as Partial< + Record + > - for (const structure of structures) { - structure.associated_satisfied_properties ??= {} - const props = prop_query.all(structure.id) - structure.associated_satisfied_properties[map] = new Set(props) - } + const associated_satisfied_properties: Partial>> = {} + for (const [map, props] of Object.entries(parsed_properties)) { + if (!props) continue + associated_satisfied_properties[map] = new Set(JSON.parse(props)) } - }) - add_associated_properties() - - return structures + return { id, name, dual, associated_satisfied_properties } + }) } /** diff --git a/shared/deduction.utils.ts b/shared/deduction.utils.ts index 4fe21763f..541c3c5cb 100644 --- a/shared/deduction.utils.ts +++ b/shared/deduction.utils.ts @@ -123,10 +123,10 @@ function is_applicable( associated_satisfied_properties?: Partial>> ) { return ( - !implication.mapped_assumptions || - Object.keys(implication.mapped_assumptions).every((key) => { + !implication.associated_assumptions || + Object.keys(implication.associated_assumptions).every((key) => { return is_subset( - implication.mapped_assumptions?.[key] ?? new Set(), + implication.associated_assumptions?.[key] ?? new Set(), associated_satisfied_properties?.[key] ?? new Set() ) }) diff --git a/shared/implications.ts b/shared/implications.ts index 9fbfb749f..3f7574954 100644 --- a/shared/implications.ts +++ b/shared/implications.ts @@ -6,7 +6,7 @@ export type NormalizedImplication = { id: string assumptions: Set conclusion: string - mapped_assumptions?: Partial>> + associated_assumptions?: Partial>> } /** @@ -30,7 +30,7 @@ export function get_normalized_implications( is_equivalence: 0 | 1 assumptions: string conclusions: string - mapped_assumptions: string + associated_assumptions: string } >( `SELECT @@ -38,7 +38,7 @@ export function get_normalized_implications( is_equivalence, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ?` ) @@ -49,9 +49,11 @@ export function get_normalized_implications( for (const impl of implications_db) { const assumptions = parse_json_set(impl.assumptions) const conclusions = parse_json_set(impl.conclusions) - const mapped_assumptions = parse_nested_json_set(impl.mapped_assumptions) + const associated_assumptions = parse_nested_json_set( + impl.associated_assumptions + ) - const has_mapped_assumptions = Object.keys(mapped_assumptions).length > 0 + const has_associated_assumptions = Object.keys(associated_assumptions).length > 0 for (const conclusion of conclusions) { const implication: NormalizedImplication = { @@ -60,8 +62,8 @@ export function get_normalized_implications( conclusion } - if (has_mapped_assumptions) { - implication.mapped_assumptions = mapped_assumptions + if (has_associated_assumptions) { + implication.associated_assumptions = associated_assumptions } implications.push(implication) @@ -75,8 +77,8 @@ export function get_normalized_implications( conclusion: assumption } - if (has_mapped_assumptions) { - implication.mapped_assumptions = mapped_assumptions + if (has_associated_assumptions) { + implication.associated_assumptions = associated_assumptions } implications.push(implication) diff --git a/src/components/ImplicationItem.svelte b/src/components/ImplicationItem.svelte index 4e4932536..066be4e0e 100644 --- a/src/components/ImplicationItem.svelte +++ b/src/components/ImplicationItem.svelte @@ -17,8 +17,8 @@ let { type, implication, highlighted_property }: Props = $props() - let has_additional_assumptions = $derived( - Object.values(implication.mapped_assumptions).some((list) => list?.size) + let has_associated_assumptions = $derived( + Object.values(implication.associated_assumptions).some((list) => list?.size) ) @@ -46,11 +46,11 @@ {/each} diff --git a/src/components/StructuresBasedOn.svelte b/src/components/StructuresBasedOn.svelte new file mode 100644 index 000000000..2eb1320f6 --- /dev/null +++ b/src/components/StructuresBasedOn.svelte @@ -0,0 +1,31 @@ + + +{#each STRUCTURE_TYPES as type} + {@const structures = structures_based_on[type]} + {#if structures && structures.length > 0} +

{capitalize(PLURALS[type])}

+ +

+ The database stores {structures.length} + {pluralize(structures.length, { + one: remove_underscores(type), + other: PLURALS[type] + })} + based on the {structure_name}. +

+ + + {/if} +{/each} diff --git a/src/lib/commons/types.ts b/src/lib/commons/types.ts index 35710c3d4..d4c5f4599 100644 --- a/src/lib/commons/types.ts +++ b/src/lib/commons/types.ts @@ -9,8 +9,15 @@ export type StructureShort = { name: string } +export type StructureShortDictionary = Partial> + export type RelatedStructure = StructureShort & { notation: string } +export type AssociatedStructure = RelatedStructure & { + label: string + associated_type: StructureType +} + export type StructureDisplay = { id: string name: string @@ -25,7 +32,7 @@ export type StructureDisplay = { parent_notation: string | null } -export type MappedTypes = Record +export type AssociatedTypes = Record export type CommentObject = { id: number; comment: string } @@ -89,7 +96,7 @@ export type ImplicationDB = { proof: string assumptions: string conclusions: string - mapped_assumptions: string + associated_assumptions: string } export type ImplicationDisplay = Replace< @@ -99,7 +106,7 @@ export type ImplicationDisplay = Replace< is_deduced: boolean assumptions: string[] conclusions: string[] - mapped_assumptions: Partial>> + associated_assumptions: Partial>> } > @@ -123,7 +130,9 @@ export type ComparisonResult = { export type StructureDetails = { type: StructureType structure: StructureDisplay + associated_structures: AssociatedStructure[] related_structures: RelatedStructure[] + structures_based_on: StructureShortDictionary children: RelatedStructure[] tags: string[] satisfied_properties: PropertyAssignmentDisplay[] @@ -139,34 +148,4 @@ export type CategorySpecificDisplay = { morphisms: string special_objects: SpecialObject[] special_morphisms: SpecialMorphism[] - stored_functors: StructureShort[] - stored_morphisms: StructureShort[] - stored_symmetric_monoidal_categories: StructureShort[] -} - -export type FunctorSpecificDisplay = { - domain: string - domain_name: string - domain_notation: string - codomain: string - codomain_name: string - codomain_notation: string - left_adjoint: string | null - left_adjoint_name: string | null - left_adjoint_notation: string | null - right_adjoint: string | null - right_adjoint_name: string | null - right_adjoint_notation: string | null -} - -export type MorphismSpecificDisplay = { - category: string - 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/consistency.ts b/src/lib/server/consistency.ts index 1e9cab31a..978298ddc 100644 --- a/src/lib/server/consistency.ts +++ b/src/lib/server/consistency.ts @@ -18,7 +18,7 @@ export function get_contradiction( } const implications = get_normalized_implications(db, type).filter( - (impl) => !impl.mapped_assumptions + (impl) => !impl.associated_assumptions ) const contradiction = contradiction_worker( diff --git a/src/lib/server/fetchers/category.ts b/src/lib/server/fetchers/category.ts index cc30693a6..7ac4fe7cc 100644 --- a/src/lib/server/fetchers/category.ts +++ b/src/lib/server/fetchers/category.ts @@ -39,46 +39,11 @@ 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 - FROM functors f - INNER JOIN structures s ON s.id = f.id - WHERE f.domain = ? OR f.codomain = ? - ORDER BY lower(s.name)` - ) - .all(id, id) - - const stored_morphisms = db - .prepare<[string], StructureShort>( - `SELECT m.id, s.name - FROM morphisms m - INNER JOIN structures s ON s.id = m.id - WHERE m.category = ? - ORDER BY lower(s.name)` - ) - .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_symmetric_monoidal_categories + special_morphisms } } diff --git a/src/lib/server/fetchers/content.ts b/src/lib/server/fetchers/content.ts index 42c4b4d22..6b665f037 100644 --- a/src/lib/server/fetchers/content.ts +++ b/src/lib/server/fetchers/content.ts @@ -3,6 +3,7 @@ import type { ImplicationDisplay, PropertyShort, StructureShort, + StructureShortDictionary, StructureType } from '$lib/commons/types' import { db } from '$lib/server/db' @@ -19,7 +20,7 @@ export function fetch_content_references(content_id: string) { ) .all(content_id) - const structures_by_type: Partial> = {} + const structures_by_type: StructureShortDictionary = {} for (const { type, ...structure } of structures) { structures_by_type[type] ??= [] @@ -51,7 +52,7 @@ export function fetch_content_references(content_id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE proof LIKE '%/content/' || ? || '%' ORDER BY lower(assumptions) || ' ' || lower(conclusions)` diff --git a/src/lib/server/fetchers/functor.ts b/src/lib/server/fetchers/functor.ts deleted file mode 100644 index 7645f72d2..000000000 --- a/src/lib/server/fetchers/functor.ts +++ /dev/null @@ -1,34 +0,0 @@ -import type { FunctorSpecificDisplay } from '$lib/commons/types' -import { db } from '$lib/server/db' -import { error } from '@sveltejs/kit' - -export function fetch_functor(id: string) { - const functor = db - .prepare<[string], FunctorSpecificDisplay>( - `SELECT - f.domain, - f.codomain, - domain.name AS domain_name, - domain.notation AS domain_notation, - codomain.name AS codomain_name, - codomain.notation AS codomain_notation, - la.id AS left_adjoint, - la.name AS left_adjoint_name, - la.notation AS left_adjoint_notation, - ra.id AS right_adjoint, - ra.name AS right_adjoint_name, - ra.notation AS right_adjoint_notation - FROM functors f - INNER JOIN structures AS domain ON domain.id = f.domain - INNER JOIN structures AS codomain ON codomain.id = f.codomain - LEFT JOIN structures AS la ON la.id = f.left_adjoint - LEFT JOIN functors AS rf ON rf.left_adjoint = f.id - LEFT JOIN structures AS ra ON ra.id = rf.id - WHERE f.id = ?` - ) - .get(id) - - if (!functor) error(404, `Could not find functor with ID '${id}'`) - - return { type: 'functor' as const, ...functor } -} diff --git a/src/lib/server/fetchers/implication.ts b/src/lib/server/fetchers/implication.ts index e0ef45a42..e537723ad 100644 --- a/src/lib/server/fetchers/implication.ts +++ b/src/lib/server/fetchers/implication.ts @@ -2,7 +2,7 @@ import { db } from '$lib/server/db' import { error } from '@sveltejs/kit' import type { ImplicationDB, - MappedTypes, + AssociatedTypes, StructureShort, StructureType } from '$lib/commons/types' @@ -21,7 +21,7 @@ export function fetch_implication(type: StructureType, id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE id = ?` ) @@ -43,19 +43,19 @@ export function fetch_implication(type: StructureType, id: string) { ) .all(type, id) - const structure_maps = db - .prepare<[StructureType], { map: string; mapped_type: StructureType }>( - `SELECT map, mapped_type - FROM structure_maps + const associated_structure_types = db + .prepare<[StructureType], { label: string; associated_type: StructureType }>( + `SELECT label, associated_type + FROM associated_structure_types WHERE type = ?` ) .all(type) - const mapped_types: MappedTypes = {} + const associated_types: AssociatedTypes = {} - for (const { map, mapped_type } of structure_maps) { - mapped_types[map] = mapped_type + for (const { label, associated_type } of associated_structure_types) { + associated_types[label] = associated_type } - return { type, implication, property_relation_dict, structures, mapped_types } + return { type, implication, property_relation_dict, structures, associated_types } } diff --git a/src/lib/server/fetchers/implications.ts b/src/lib/server/fetchers/implications.ts index 37a1e301e..a4077f90b 100644 --- a/src/lib/server/fetchers/implications.ts +++ b/src/lib/server/fetchers/implications.ts @@ -12,7 +12,7 @@ export function fetch_implications(type: StructureType) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ? ORDER BY lower(assumptions) || ' ' || lower(conclusions)` diff --git a/src/lib/server/fetchers/missing_data.ts b/src/lib/server/fetchers/missing_data.ts index 47d58cbaf..93bc435e5 100644 --- a/src/lib/server/fetchers/missing_data.ts +++ b/src/lib/server/fetchers/missing_data.ts @@ -78,7 +78,7 @@ export function fetch_missing_data(type: StructureType) { ) const implications = get_normalized_implications(db, type).filter( - (impl) => !impl.mapped_assumptions + (impl) => !impl.associated_assumptions ) const witnessed_pairs_set = new Set(witnessed_pairs.map(({ p, q }) => `${p}|${q}`)) diff --git a/src/lib/server/fetchers/morphism.ts b/src/lib/server/fetchers/morphism.ts deleted file mode 100644 index 8aacbf9a8..000000000 --- a/src/lib/server/fetchers/morphism.ts +++ /dev/null @@ -1,21 +0,0 @@ -import type { MorphismSpecificDisplay } from '$lib/commons/types' -import { db } from '$lib/server/db' -import { error } from '@sveltejs/kit' - -export function fetch_morphism(id: string) { - const morphism = db - .prepare<[string], MorphismSpecificDisplay>( - `SELECT - c.id AS category, - c.name AS category_name, - c.notation AS category_notation - FROM morphisms m - INNER JOIN structures AS c ON c.id = m.category - WHERE m.id = ?` - ) - .get(id) - - if (!morphism) error(404, `Could not find morphism with ID '${id}'`) - - return { type: 'morphism' as const, ...morphism } -} diff --git a/src/lib/server/fetchers/property.ts b/src/lib/server/fetchers/property.ts index a903c975d..3486723f3 100644 --- a/src/lib/server/fetchers/property.ts +++ b/src/lib/server/fetchers/property.ts @@ -60,7 +60,7 @@ export function fetch_property(type: StructureType, id: string) { proof, assumptions, conclusions, - mapped_assumptions + associated_assumptions FROM implications_view WHERE type = ? AND ( diff --git a/src/lib/server/fetchers/structure.ts b/src/lib/server/fetchers/structure.ts index b4727cb33..5b279865e 100644 --- a/src/lib/server/fetchers/structure.ts +++ b/src/lib/server/fetchers/structure.ts @@ -6,7 +6,9 @@ import type { StructureDetails, StructureDisplay, StructureShort, - StructureType + StructureShortDictionary, + StructureType, + AssociatedStructure } from '$lib/commons/types' import { error } from '@sveltejs/kit' import { db } from '$lib/server/db' @@ -38,6 +40,21 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai error(404, `Could not find ${type} with ID '${id}'`) } + const associated_structures = db + .prepare<[string], AssociatedStructure>( + `SELECT + s.id, + s.name, + s.notation, + a.label, + a.associated_type + FROM associated_structures a + INNER JOIN structures s + ON s.id = a.associated_structure_id + WHERE a.structure_id = ?` + ) + .all(id) + const related_structures = db .prepare<[string], RelatedStructure>( `SELECT @@ -51,6 +68,29 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai ) .all(id) + const list_structures_based_on = db + .prepare<[string], StructureShort & { type: StructureType }>( + `SELECT DISTINCT s.id, s.name, a.type + FROM associated_structures a + INNER JOIN structures s + ON s.id = a.structure_id + INNER JOIN associated_structure_types m + ON + m.label = a.label + AND m.type = a.type + AND m.associated_type = a.associated_type + WHERE a.associated_structure_id = ? AND m.required = TRUE + ORDER BY a.type, lower(s.name)` + ) + .all(id) + + const structures_based_on: StructureShortDictionary = {} + + for (const { id, name, type } of list_structures_based_on) { + structures_based_on[type] ??= [] + structures_based_on[type].push({ id, name }) + } + const children = db .prepare<[string], RelatedStructure>( `SELECT s.id, s.name, s.notation @@ -147,6 +187,8 @@ export function fetch_structure(type: StructureType, id: string): StructureDetai structure, children, related_structures, + associated_structures, + structures_based_on, tags, satisfied_properties, unsatisfied_properties, diff --git a/src/lib/server/fetchers/symmetric_monoidal_category.ts b/src/lib/server/fetchers/symmetric_monoidal_category.ts deleted file mode 100644 index 89cb454c3..000000000 --- a/src/lib/server/fetchers/symmetric_monoidal_category.ts +++ /dev/null @@ -1,21 +0,0 @@ -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/lib/server/transforms.ts b/src/lib/server/transforms.ts index 46ca3ab6f..aff337e0f 100644 --- a/src/lib/server/transforms.ts +++ b/src/lib/server/transforms.ts @@ -4,9 +4,10 @@ import type { PropertyAssignmentDB, PropertyAssignmentDisplay, ImplicationDB, - ImplicationDisplay + ImplicationDisplay, + StructureDetails } from '$lib/commons/types' -import { parse_nested_json_set } from '$shared/utils' +import { add_math, parse_nested_json_set, strip_math } from '$shared/utils' export function display_property(property: PropertyDB): PropertyDisplay { return { @@ -38,6 +39,16 @@ export function display_implication(implication: ImplicationDB): ImplicationDisp proof: implication.proof, assumptions: JSON.parse(implication.assumptions), conclusions: JSON.parse(implication.conclusions), - mapped_assumptions: parse_nested_json_set(implication.mapped_assumptions) + associated_assumptions: parse_nested_json_set(implication.associated_assumptions) } } + +export function adjust_functor_notation(functor: StructureDetails) { + const domain = functor.associated_structures.find((s) => s.label == 'domain') + const codomain = functor.associated_structures.find((s) => s.label == 'codomain') + if (!domain || !codomain) return + + functor.structure.notation = add_math( + `${strip_math(functor.structure.notation)}: ${strip_math(domain.notation)} \\to ${strip_math(codomain.notation)}` + ) +} diff --git a/src/pages/CategoryDetailPage.svelte b/src/pages/CategoryDetailPage.svelte index 9e8c8a9cf..5f58f804a 100644 --- a/src/pages/CategoryDetailPage.svelte +++ b/src/pages/CategoryDetailPage.svelte @@ -1,7 +1,5 @@ - - - {#snippet definition()} -
  • - Domain: - {data.domain_name} -
    • - -
  • - Codomain: - {data.codomain_name} -
    • - - {#if data.left_adjoint} -
  • - Left adjoint functor: - - {@html data.left_adjoint_notation} - -
    • - {/if} - - {#if data.right_adjoint} -
  • - Right adjoint functor: - - {@html data.right_adjoint_notation} - -
    • - {/if} - {/snippet} -     diff --git a/src/pages/ImplicationPage.svelte b/src/pages/ImplicationPage.svelte index 06f29490b..4f1cd8536 100644 --- a/src/pages/ImplicationPage.svelte +++ b/src/pages/ImplicationPage.svelte @@ -6,8 +6,8 @@ import { get_property_url } from '$shared/property.utils' import type { ImplicationDisplay, - MappedTypes, StructureShort, + AssociatedTypes, StructureType } from '$lib/commons/types' import { PLURALS } from '$shared/config' @@ -16,15 +16,20 @@ type: StructureType implication: ImplicationDisplay structures: StructureShort[] - mapped_types: MappedTypes + associated_types: AssociatedTypes property_relation_dict: Record> } - let { type, implication, structures, mapped_types, property_relation_dict }: Props = - $props() + let { + type, + implication, + structures, + associated_types, + property_relation_dict + }: Props = $props() - let has_additional_assumptions = $derived( - Object.values(implication.mapped_assumptions).some((list) => list?.size) + let has_associated_assumptions = $derived( + Object.values(implication.associated_assumptions).some((list) => list?.size) ) @@ -34,19 +39,20 @@

    Claim: - {#if has_additional_assumptions} + {#if has_associated_assumptions} Given a {remove_underscores(type)} - {#each Object.entries(implication.mapped_assumptions) as [map, set], ind} + {#each Object.entries(implication.associated_assumptions) as [label, set], ind} {#if set} whose - {remove_underscores(map)} + {remove_underscores(label)} {#each set as property, index} - {property_relation_dict[mapped_types[map]][property]} - {property}{property}{#if index < set.size - 1}  and  {/if} - {/each}{#if ind < Object.entries(implication.mapped_assumptions).length - 1} + {/each}{#if ind < Object.entries(implication.associated_assumptions).length - 1} , and  {/if} {/if} diff --git a/src/pages/MorphismDetailPage.svelte b/src/pages/MorphismDetailPage.svelte deleted file mode 100644 index fc15a3b83..000000000 --- a/src/pages/MorphismDetailPage.svelte +++ /dev/null @@ -1,19 +0,0 @@ - - - - {#snippet definition()} -

  • - Category: - - {data.category_name} - -
    • - {/snippet} - diff --git a/src/pages/StructureDetailPage.svelte b/src/pages/StructureDetailPage.svelte index fd486540c..7cc8a2a8e 100644 --- a/src/pages/StructureDetailPage.svelte +++ b/src/pages/StructureDetailPage.svelte @@ -5,23 +5,28 @@ import SuggestionForm from '$components/SuggestionForm.svelte' import TagList from '$components/TagList.svelte' import IndistinguishableStructures from '$components/IndistinguishableStructures.svelte' + import StructuresBasedOn from '$components/StructuresBasedOn.svelte' import { PLURALS } from '$shared/config' import type { + AssociatedStructure, CommentObject, PropertyAssignmentDisplay, PropertyShort, RelatedStructure, StructureDisplay, StructureShort, + StructureShortDictionary, StructureType } from '$lib/commons/types' import type { Snippet } from 'svelte' - import { remove_underscores } from '$shared/utils' + import { capitalize, remove_underscores } from '$shared/utils' type Props = { type: StructureType structure: StructureDisplay + associated_structures: AssociatedStructure[] related_structures: RelatedStructure[] + structures_based_on: StructureShortDictionary children: RelatedStructure[] tags: string[] satisfied_properties: PropertyAssignmentDisplay[] @@ -32,13 +37,14 @@ comments: CommentObject[] definition?: Snippet specials?: Snippet - footer?: Snippet } let { type, structure, + associated_structures, related_structures, + structures_based_on, children, tags, satisfied_properties, @@ -48,8 +54,7 @@ indistinguishable_structures, comments, definition, - specials, - footer + specials }: Props = $props() @@ -68,6 +73,13 @@ {@render definition?.()} + {#each associated_structures as a} +
  • + {capitalize(remove_underscores(a.label))}: + {a.name} +
    • + {/each} + {#if structure.parent}
  • Parent: @@ -143,7 +155,7 @@ -{@render footer?.()} + diff --git a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte b/src/pages/SymmetricMonoidalCategoryDetailPage.svelte deleted file mode 100644 index 6213f9c07..000000000 --- a/src/pages/SymmetricMonoidalCategoryDetailPage.svelte +++ /dev/null @@ -1,22 +0,0 @@ - - - - {#snippet definition()} -
  • - Underlying category: - - {data.underlying_category_name} - -
    • - {/snippet} - diff --git a/src/routes/[type]/[id]/+page.server.ts b/src/routes/[type]/[id]/+page.server.ts index 58af8b25c..73d2ace54 100644 --- a/src/routes/[type]/[id]/+page.server.ts +++ b/src/routes/[type]/[id]/+page.server.ts @@ -3,17 +3,7 @@ import { fetch_structure } from '$lib/server/fetchers/structure' import { is_structure_type } from '$shared/config' import { error } from '@sveltejs/kit' 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, - symmetric_monoidal_category: fetch_symmetric_monoidal_category -} +import { adjust_functor_notation } from '$lib/server/transforms' export const load = (event) => { const type = event.params.type @@ -23,13 +13,9 @@ export const load = (event) => { const structure_data = fetch_structure(type, id) - const special_structure_data = special_fetchers[type](id) + if (type === 'functor') adjust_functor_notation(structure_data) - if (special_structure_data.type === 'functor') { - structure_data.structure.notation = add_math( - `${strip_math(structure_data.structure.notation)}: ${strip_math(special_structure_data.domain_notation)} \\to ${strip_math(special_structure_data.codomain_notation)}` - ) - } + const special_structure_data = type === 'category' ? fetch_category(id) : { type } return render_nested_formulas({ structure_data, diff --git a/src/routes/[type]/[id]/+page.svelte b/src/routes/[type]/[id]/+page.svelte index da567a1e3..51e3acc60 100644 --- a/src/routes/[type]/[id]/+page.svelte +++ b/src/routes/[type]/[id]/+page.svelte @@ -1,29 +1,12 @@ - - {#if data.special_structure_data.type === 'category'} -{/if} - -{#if data.special_structure_data.type === 'functor'} - -{/if} - -{#if data.special_structure_data.type === 'morphism'} - -{/if} - -{#if data.special_structure_data.type === 'symmetric_monoidal_category'} - +{:else} + {/if}