ScriptRaccoon · ScriptRaccoon · Aug 15, 2026 · Aug 14, 2026 · Aug 14, 2026 · Aug 14, 2026
diff --git 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.
 
-<img alt="database diagram" src="https://github.com/user-attachments/assets/72da5e08-3eaf-48f4-9e00-bd0d865a2c92" />
+<img alt="database diagram" src="https://github.com/user-attachments/assets/a2cb788e-cac0-44c6-80fc-ae07de2fe83a" />
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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