From 9a9c27c55b399c19c763863634141dd64df3ce9a Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 03:52:41 +0200
Subject: [PATCH 01/13] show only tags on list page that are actually used

---
 src/lib/server/fetchers/structures.ts | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/lib/server/fetchers/structures.ts b/src/lib/server/fetchers/structures.ts
index d61ee10e..2fc4af8c 100644
--- a/src/lib/server/fetchers/structures.ts
+++ b/src/lib/server/fetchers/structures.ts
@@ -26,10 +26,14 @@ export function fetch_structures_and_tags(type: StructureType) {
             WHERE type = ${type}
             ORDER BY lower(name)`,
 		sql`
-            SELECT tag
-            FROM tags
-            WHERE type = ${type}
-            ORDER BY id
+            SELECT t.tag
+            FROM tags t
+            WHERE t.type = ${type}
+            AND EXISTS (
+                SELECT 1 FROM structure_tag_assignments a
+                WHERE a.tag = t.tag AND a.type = ${type}
+            )
+            ORDER BY t.id
         `,
 	])
 

From 35861ec0d8ed0c65f16c8ffb9dcb4adc1a2fb899 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 00:27:54 +0200
Subject: [PATCH 02/13] functor detail page: make clear that the functor is not
 itself a left/right adjoint necessarily

---
 src/routes/functor/[id]/+page.svelte | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/routes/functor/[id]/+page.svelte b/src/routes/functor/[id]/+page.svelte
index 5b7bc43d..6d75a430 100644
--- a/src/routes/functor/[id]/+page.svelte
+++ b/src/routes/functor/[id]/+page.svelte
@@ -18,7 +18,7 @@
 
 		{#if data.functor.left_adjoint}
 			<li>
-				<strong>Left adjoint:</strong>
+				<strong>Left adjoint functor:</strong>
 				<a
 					href="/functor/{data.functor.left_adjoint}"
 					aria-label={data.functor.left_adjoint_name}
@@ -30,7 +30,7 @@
 
 		{#if data.functor.right_adjoint}
 			<li>
-				<strong>Right adjoint:</strong>
+				<strong>Right adjoint functor:</strong>
 				<a
 					href="/functor/{data.functor.right_adjoint}"
 					aria-label={data.functor.right_adjoint_name}

From eee0412d1dd721e2165393fd481590c49642badc Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 01:29:59 +0200
Subject: [PATCH 03/13] write mapped assumptions in generated proofs

---
 databases/catdat/scripts/utils/implications.ts | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/databases/catdat/scripts/utils/implications.ts b/databases/catdat/scripts/utils/implications.ts
index f0388769..87d7f9e9 100644
--- a/databases/catdat/scripts/utils/implications.ts
+++ b/databases/catdat/scripts/utils/implications.ts
@@ -93,12 +93,23 @@ function get_assumption_string(
 ): string {
 	const { assumptions } = implication
 
-	return Array.from(assumptions)
+	const own = Array.from(assumptions)
 		.map(
 			(assumption) =>
 				`${properties_dict[assumption][conditional ? 'conditional_relation' : 'relation']} ${assumption}`,
 		)
 		.join(' and ')
+
+	if (!implication.mapped_assumptions) return own
+
+	const mapped = Object.entries(implication.mapped_assumptions)
+		.map(
+			([map, props]) =>
+				`and the ${map} has the required properties (${Array.from(props!).join(', ')})`,
+		)
+		.join(', ')
+
+	return `${own}, ${mapped}`
 }
 
 function get_conclusion_string(

From 1fa3c76d0ea347cd853653c4ac7711f6b67273a4 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 03:54:14 +0200
Subject: [PATCH 04/13] weaken assumption for saft: locally ess. small suffices

---
 databases/catdat/data/functor-implications/adjoints.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/databases/catdat/data/functor-implications/adjoints.yaml b/databases/catdat/data/functor-implications/adjoints.yaml
index abd14f5b..f7c6fd2c 100644
--- a/databases/catdat/data/functor-implications/adjoints.yaml
+++ b/databases/catdat/data/functor-implications/adjoints.yaml
@@ -13,10 +13,10 @@
     source:
       - cogenerating set
       - complete
-      - locally small
+      - locally essentially small
       - well-powered
     target:
-      - locally small
+      - locally essentially small
   conclusions:
     - right adjoint
   proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the <a href="https://ncatlab.org/nlab/show/adjoint+functor+theorem" target="_blank">nLab</a>, or in <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 8.2.

From 7ebf9d07e1318970b5b4cc995b6c0e0845b4d2b8 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 04:53:22 +0200
Subject: [PATCH 05/13] add property: fully faithful

---
 .cspell.json                                       |  1 +
 .../data/functor-implications/equivalences.yaml    |  3 +--
 .../catdat/data/functor-implications/misc.yaml     | 14 +++++++++++---
 .../catdat/data/functor-properties/faithful.yaml   |  1 +
 databases/catdat/data/functor-properties/full.yaml |  1 +
 .../data/functor-properties/fully faithful.yaml    | 10 ++++++++++
 .../scripts/expected-data/forget_vector.json       |  1 +
 databases/catdat/scripts/expected-data/id_Set.json |  1 +
 8 files changed, 27 insertions(+), 5 deletions(-)
 create mode 100644 databases/catdat/data/functor-properties/fully faithful.yaml

diff --git a/.cspell.json b/.cspell.json
index f8726064..df420421 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -100,6 +100,7 @@
 		"coquotients",
 		"coreflection",
 		"coreflective",
+		"coreflector",
 		"coreflexive",
 		"coreflexivity",
 		"coregular",
diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml
index c9f1916a..27defcc3 100644
--- a/databases/catdat/data/functor-implications/equivalences.yaml
+++ b/databases/catdat/data/functor-implications/equivalences.yaml
@@ -1,8 +1,7 @@
 - id: equivalence_criterion
   assumptions:
     - essentially surjective
-    - faithful
-    - full
+    - fully faithful
   conclusions:
     - equivalence
   proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IV, Theorem 4.1.
diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml
index bed2217c..995eb0aa 100644
--- a/databases/catdat/data/functor-implications/misc.yaml
+++ b/databases/catdat/data/functor-implications/misc.yaml
@@ -1,3 +1,12 @@
+- id: fully-faithful-definition
+  assumptions:
+    - full
+    - faithful
+  conclusions:
+    - fully faithful
+  proof: This holds by definition.
+  is_equivalence: true
+
 - id: faithful-via-equalizers
   assumptions:
     - conservative
@@ -12,8 +21,7 @@
 
 - id: conservative_consequences
   assumptions:
-    - full
-    - faithful
+    - fully faithful
   conclusions:
     - conservative
   proof: If $F(f)$ is an isomorphism, its inverse has the form $F(g)$ since $F$ is full. Since $F$ is faithful, it follows that $f$ is inverse to $g$.
@@ -35,5 +43,5 @@
     - faithful
     - essentially injective
     - conservative
-  proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is am morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.'
+  proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is a morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.'
   is_equivalence: false
diff --git a/databases/catdat/data/functor-properties/faithful.yaml b/databases/catdat/data/functor-properties/faithful.yaml
index 2dc054aa..f50df43f 100644
--- a/databases/catdat/data/functor-properties/faithful.yaml
+++ b/databases/catdat/data/functor-properties/faithful.yaml
@@ -7,5 +7,6 @@ dual_property: faithful
 related_properties:
   - equivalence
   - full
+  - fully faithful
   - essentially injective
   - left-invertible
diff --git a/databases/catdat/data/functor-properties/full.yaml b/databases/catdat/data/functor-properties/full.yaml
index c7747d34..74cee52c 100644
--- a/databases/catdat/data/functor-properties/full.yaml
+++ b/databases/catdat/data/functor-properties/full.yaml
@@ -7,4 +7,5 @@ dual_property: full
 related_properties:
   - equivalence
   - faithful
+  - fully faithful
   - essentially injective
diff --git a/databases/catdat/data/functor-properties/fully faithful.yaml b/databases/catdat/data/functor-properties/fully faithful.yaml
new file mode 100644
index 00000000..37a55bfa
--- /dev/null
+++ b/databases/catdat/data/functor-properties/fully faithful.yaml	
@@ -0,0 +1,10 @@
+id: fully faithful
+relation: is
+description: 'A functor is <i>fully faithful</i> when it is full and faithful. This means that for all objects $A,B$ in its domain the map $\Hom(A,B) \to \Hom(F(A),F(B))$, $f \mapsto F(f)$ is a bijection.'
+nlab_link: https://ncatlab.org/nlab/show/full+and+faithful+functor
+invariant_under_equivalences: true
+dual_property: fully faithful
+related_properties:
+  - full
+  - faithful
+  - equivalence
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index e45b70b6..1fee1ac8 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -8,6 +8,7 @@
 	"exact": false,
 	"preserves finite coproducts": false,
 	"full": false,
+	"fully faithful": false,
 	"preserves initial objects": false,
 	"left adjoint": false,
 	"right exact": false,
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index 486c2879..4fec7eb3 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -16,6 +16,7 @@
 	"preserves finite coproducts": true,
 	"preserves finite products": true,
 	"full": true,
+	"fully faithful": true,
 	"preserves initial objects": true,
 	"left adjoint": true,
 	"left exact": true,

From afb4639f98ab7de2b371150c8078e9b28001fe04 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 05:30:17 +0200
Subject: [PATCH 06/13] add property: right-invertible

---
 .../data/functor-implications/equivalences.yaml   | 15 +++++++++++++--
 .../catdat/data/functor-implications/misc.yaml    |  8 ++++++++
 .../data/functor-properties/left-invertible.yaml  |  3 ++-
 .../data/functor-properties/right-invertible.yaml | 10 ++++++++++
 .../catdat/data/functors/abelianization.yaml      |  3 +++
 .../catdat/data/functors/coproduct_sets.yaml      |  4 ++--
 .../catdat/data/functors/enveloping_group.yaml    |  2 +-
 .../catdat/data/functors/forget_topology.yaml     |  4 ++--
 databases/catdat/data/functors/group_units.yaml   |  4 ++--
 databases/catdat/data/functors/product_sets.yaml  |  4 ++--
 .../scripts/expected-data/forget_vector.json      |  1 +
 .../catdat/scripts/expected-data/id_Set.json      |  3 ++-
 12 files changed, 48 insertions(+), 13 deletions(-)
 create mode 100644 databases/catdat/data/functor-properties/right-invertible.yaml

diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml
index 27defcc3..de29a9dc 100644
--- a/databases/catdat/data/functor-implications/equivalences.yaml
+++ b/databases/catdat/data/functor-implications/equivalences.yaml
@@ -7,11 +7,22 @@
   proof: This is standard, see <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. IV, Theorem 4.1.
   is_equivalence: true
 
-- id: equivalence_consequences
+- id: equivalence_invertible
   assumptions:
     - equivalence
   conclusions:
-    - monadic
     - left-invertible
+    - right-invertible
+  proof: >-
+    If a functor $F$ has a right inverse $R$ and a left inverse $L$, then
+    $$L \cong L \circ F \circ R \cong R.$$
+    Hence, $R$ (and $L$) are (pseudo-)inverse to $F$.
+  is_equivalence: true
+
+- id: equivalence_monadic
+  assumptions:
+    - equivalence
+  conclusions:
+    - monadic
   proof: This is easy.
   is_equivalence: false
diff --git a/databases/catdat/data/functor-implications/misc.yaml b/databases/catdat/data/functor-implications/misc.yaml
index 995eb0aa..e3d52935 100644
--- a/databases/catdat/data/functor-implications/misc.yaml
+++ b/databases/catdat/data/functor-implications/misc.yaml
@@ -45,3 +45,11 @@
     - conservative
   proof: 'Let $G : \D \to \C$ be a left-inverse to $F : \C \to \D$, meaning that $G \circ F \cong \id_{\C}$. Then $F(A) \cong F(B)$ implies $A \cong G(F(A)) \cong G(F(B)) \cong B$ for all $A,B \in \C$. Thus, $F$ essentially injective. Moreover, since $G \circ F$ is faithful, the composed map $\Hom(A,B) \to \Hom(F(A),F(B)) \to \Hom(G(F(A)),G(F(B))$ is injective, so that also $\Hom(A,B) \to \Hom(F(A),F(B))$ is injective. This shows that $F$ is faithful. Finally, if $f : A \to B$ is a morphism such that $F(f)$ is an isomorphism, then $G(F(f))$ is an isomorphism. Since $G(F(f)) \cong f$ in $\Mor(\C)$, we conclude that $f$ is an isomorphism. Therefore, $F$ is conservative.'
   is_equivalence: false
+
+- id: right-invertible_consequences
+  assumptions:
+    - right-invertible
+  conclusions:
+    - essentially surjective
+  proof: This is trivial.
+  is_equivalence: false
diff --git a/databases/catdat/data/functor-properties/left-invertible.yaml b/databases/catdat/data/functor-properties/left-invertible.yaml
index 081bb50d..82282809 100644
--- a/databases/catdat/data/functor-properties/left-invertible.yaml
+++ b/databases/catdat/data/functor-properties/left-invertible.yaml
@@ -1,6 +1,6 @@
 id: left-invertible
 relation: is
-description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse.'
+description: 'A <i>left inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $G \circ F \cong \id_{\C}$. We do not require $G \circ F = \id_{\C}$ here, which is often too strict. A functor is called <i>left-invertible</i> when it has a left inverse. This notion is self-dual in the sense that $F : \C \to \D$ is left-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is left-invertible.'
 nlab_link: https://ncatlab.org/nlab/show/inverse+functor
 invariant_under_equivalences: true
 dual_property: left-invertible
@@ -8,3 +8,4 @@ related_properties:
   - equivalence
   - faithful
   - essentially injective
+  - right-invertible
diff --git a/databases/catdat/data/functor-properties/right-invertible.yaml b/databases/catdat/data/functor-properties/right-invertible.yaml
new file mode 100644
index 00000000..1f7adc39
--- /dev/null
+++ b/databases/catdat/data/functor-properties/right-invertible.yaml
@@ -0,0 +1,10 @@
+id: right-invertible
+relation: is
+description: 'A <i>right inverse</i> of a functor $F : \C \to \D$ is a functor $G : \D \to \C$ satisfying $F \circ G \cong \id_{\D}$. We do not require $F \circ G = \id_{\D}$ here, which is often too strict. A functor is called <i>right-invertible</i> when it has a right inverse. This notion is self-dual in the sense that $F : \C \to \D$ is right-invertible iff $F^{\op} : \C^{\op} \to \D^{\op}$ is right-invertible.'
+nlab_link: https://ncatlab.org/nlab/show/inverse+functor
+invariant_under_equivalences: true
+dual_property: right-invertible
+related_properties:
+  - equivalence
+  - essentially surjective
+  - left-invertible
diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml
index d6b54547..9a2ba701 100644
--- a/databases/catdat/data/functors/abelianization.yaml
+++ b/databases/catdat/data/functors/abelianization.yaml
@@ -16,6 +16,9 @@ satisfied_properties:
   - property: left adjoint
     proof: This functor is left adjoint to the forgetful functor.
 
+  - property: right-invertible
+    proof: The forgetful functor provides a right inverse.
+
   - property: essentially surjective
     proof: For abelian groups $G$ we have $G \cong G^{\ab}$.
 
diff --git a/databases/catdat/data/functors/coproduct_sets.yaml b/databases/catdat/data/functors/coproduct_sets.yaml
index e51c2c75..9bf41bc0 100644
--- a/databases/catdat/data/functors/coproduct_sets.yaml
+++ b/databases/catdat/data/functors/coproduct_sets.yaml
@@ -14,8 +14,8 @@ related_functors:
   - product_sets
 
 satisfied_properties:
-  - property: essentially surjective
-    proof: We have $X \cong X + 0$.
+  - property: right-invertible
+    proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,0)$ provides a right inverse since $X + 0 \cong X$.
 
   - property: preserves equalizers
     proof: This can be checked with a straight forward calculation.
diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml
index f11b97ae..c54b6236 100644
--- a/databases/catdat/data/functors/enveloping_group.yaml
+++ b/databases/catdat/data/functors/enveloping_group.yaml
@@ -17,7 +17,7 @@ satisfied_properties:
   - property: left adjoint
     proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \to \Mon$.'
 
-  - property: essentially surjective
+  - property: right-invertible
     proof: 'In fact, the counit of the adjunction $F \circ U_{\Grp,\Mon} \to \id_{\Grp}$ is an isomorphism since the right adjoint $U_{\Grp,\Mon}$ is fully faithful (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
 
   - property: preserves finite products
diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml
index f129178b..2d987131 100644
--- a/databases/catdat/data/functors/forget_topology.yaml
+++ b/databases/catdat/data/functors/forget_topology.yaml
@@ -20,8 +20,8 @@ satisfied_properties:
   - property: representable
     proof: This functor is represented by the singleton space.
 
-  - property: essentially surjective
-    proof: Every set can be equipped with the discrete topology.
+  - property: right-invertible
+    proof: 'The functor $D : \Set \to \Top$ that endows a set with the discrete topology provides a right inverse. Remark: Another right inverse functor can be defined with the indiscrete topology. These are the only right inverses (up to isomorphism) by <a href="https://math.stackexchange.com/questions/4368730" target="_blank">MSE/4368730</a>.'
 
   - property: left adjoint
     proof: 'The indiscrete topology defines a functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.'
diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml
index c223cba4..cd0ad5e4 100644
--- a/databases/catdat/data/functors/group_units.yaml
+++ b/databases/catdat/data/functors/group_units.yaml
@@ -13,8 +13,8 @@ tags:
 related_functors: []
 
 satisfied_properties:
-  - property: essentially surjective
-    proof: If $G$ is a group, then $G$ is isomorphic to its group of units.
+  - property: right-invertible
+    proof: The forgetful functor provides a right inverse, since the group of units of a group $G$ is isomorphic to $G$.
 
   - property: right adjoint
     proof: This functor is right adjoint to the forgetful functor $\Grp \to \Mon$.
diff --git a/databases/catdat/data/functors/product_sets.yaml b/databases/catdat/data/functors/product_sets.yaml
index 0e7e1958..9e32c27d 100644
--- a/databases/catdat/data/functors/product_sets.yaml
+++ b/databases/catdat/data/functors/product_sets.yaml
@@ -15,8 +15,8 @@ related_functors:
   - coproduct_sets
 
 satisfied_properties:
-  - property: essentially surjective
-    proof: We have $X \cong X \times 1$.
+  - property: right-invertible
+    proof: The functor $\Set \to \Set \times \Set$, $X \mapsto (X,1)$ provides a right inverse since $X \times 1 \cong X$.
 
   - property: preserves initial objects
     proof: This is obvious.
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index 1fee1ac8..b77bf4a1 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -14,6 +14,7 @@
 	"right exact": false,
 	"essentially injective": false,
 	"left-invertible": false,
+	"right-invertible": false,
 
 	"cofinitary": true,
 	"conservative": true,
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index 4fec7eb3..9ade56ee 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -30,5 +30,6 @@
 	"preserves reflexive coequalizers": true,
 	"preserves coreflexive equalizers": true,
 	"essentially injective": true,
-	"left-invertible": true
+	"left-invertible": true,
+	"right-invertible": true
 }

From 9634358d628a5f81acb2f521d21758261c6004ee Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 23:26:49 +0200
Subject: [PATCH 07/13] add property: is a reflector

---
 .../catdat/data/functor-implications/adjoints.yaml   |  9 +++++++++
 .../data/functor-implications/equivalences.yaml      |  1 +
 .../catdat/data/functor-properties/left adjoint.yaml |  1 +
 .../catdat/data/functor-properties/reflector.yaml    |  9 +++++++++
 .../data/functor-properties/representable.yaml       |  1 -
 .../data/functor-properties/right-invertible.yaml    |  1 +
 databases/catdat/data/functors/abelianization.yaml   | 10 ++--------
 databases/catdat/data/functors/coproduct_sets.yaml   |  5 ++++-
 databases/catdat/data/functors/enveloping_group.yaml |  7 ++-----
 databases/catdat/data/functors/forget_topology.yaml  | 12 ++++++------
 .../catdat/scripts/expected-data/forget_vector.json  |  1 +
 databases/catdat/scripts/expected-data/id_Set.json   |  3 ++-
 12 files changed, 38 insertions(+), 22 deletions(-)
 create mode 100644 databases/catdat/data/functor-properties/reflector.yaml

diff --git a/databases/catdat/data/functor-implications/adjoints.yaml b/databases/catdat/data/functor-implications/adjoints.yaml
index f7c6fd2c..ba69f290 100644
--- a/databases/catdat/data/functor-implications/adjoints.yaml
+++ b/databases/catdat/data/functor-implications/adjoints.yaml
@@ -21,3 +21,12 @@
     - right adjoint
   proof: This is the Special Adjoint Functor Theorem. The proof can be found, for example, at the <a href="https://ncatlab.org/nlab/show/adjoint+functor+theorem" target="_blank">nLab</a>, or in <a href="https://ncatlab.org/nlab/show/Categories+for+the+Working+Mathematician" target="_blank">Mac Lane</a>, Ch. V, Theorem 8.2.
   is_equivalence: false
+
+- id: reflector_consequences
+  assumptions:
+    - reflector
+  conclusions:
+    - left adjoint
+    - right-invertible
+  proof: 'If $F : \C \to \D$ is a reflector, it is left adjoint to a fully faithful functor $G : \D \to \C$. Thus, the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>). This shows that $G$ is a right inverse of $F$.'
+  is_equivalence: false
diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml
index de29a9dc..84dd3892 100644
--- a/databases/catdat/data/functor-implications/equivalences.yaml
+++ b/databases/catdat/data/functor-implications/equivalences.yaml
@@ -24,5 +24,6 @@
     - equivalence
   conclusions:
     - monadic
+    - reflector
   proof: This is easy.
   is_equivalence: false
diff --git a/databases/catdat/data/functor-properties/left adjoint.yaml b/databases/catdat/data/functor-properties/left adjoint.yaml
index 810f29cb..c2675966 100644
--- a/databases/catdat/data/functor-properties/left adjoint.yaml	
+++ b/databases/catdat/data/functor-properties/left adjoint.yaml	
@@ -7,3 +7,4 @@ dual_property: right adjoint
 related_properties:
   - cocontinuous
   - comonadic
+  - reflector
diff --git a/databases/catdat/data/functor-properties/reflector.yaml b/databases/catdat/data/functor-properties/reflector.yaml
new file mode 100644
index 00000000..55a9fc8b
--- /dev/null
+++ b/databases/catdat/data/functor-properties/reflector.yaml
@@ -0,0 +1,9 @@
+id: reflector
+relation: is a
+description: 'A functor $F : \C \to \D$ is a <i>reflector</i> if it is left adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full reflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
+nlab_link: https://ncatlab.org/nlab/show/reflective+subcategory
+invariant_under_equivalences: true
+# dual_property: null FIXME
+related_properties:
+  - left adjoint
+  - right-invertible
diff --git a/databases/catdat/data/functor-properties/representable.yaml b/databases/catdat/data/functor-properties/representable.yaml
index bec89ed0..e5ec76db 100644
--- a/databases/catdat/data/functor-properties/representable.yaml
+++ b/databases/catdat/data/functor-properties/representable.yaml
@@ -3,6 +3,5 @@ relation: is
 description: 'A functor $F : \C \to \D$ is <i>representable</i> if $\C$ is locally small, $\D = \Set$, and there is an object $A \in \C$ with $F \cong \Hom(A,-)$.'
 nlab_link: https://ncatlab.org/nlab/show/representable+functor
 invariant_under_equivalences: true
-dual_property: null
 related_properties:
   - continuous
diff --git a/databases/catdat/data/functor-properties/right-invertible.yaml b/databases/catdat/data/functor-properties/right-invertible.yaml
index 1f7adc39..b5a8c90e 100644
--- a/databases/catdat/data/functor-properties/right-invertible.yaml
+++ b/databases/catdat/data/functor-properties/right-invertible.yaml
@@ -8,3 +8,4 @@ related_properties:
   - equivalence
   - essentially surjective
   - left-invertible
+  - reflector
diff --git a/databases/catdat/data/functors/abelianization.yaml b/databases/catdat/data/functors/abelianization.yaml
index 9a2ba701..c79996e5 100644
--- a/databases/catdat/data/functors/abelianization.yaml
+++ b/databases/catdat/data/functors/abelianization.yaml
@@ -13,14 +13,8 @@ tags:
 related_functors: []
 
 satisfied_properties:
-  - property: left adjoint
-    proof: This functor is left adjoint to the forgetful functor.
-
-  - property: right-invertible
-    proof: The forgetful functor provides a right inverse.
-
-  - property: essentially surjective
-    proof: For abelian groups $G$ we have $G \cong G^{\ab}$.
+  - property: reflector
+    proof: 'This functor is left adjoint to the forgetful functor $U_{\Ab,\Grp} : \Ab \hookrightarrow \Grp$, which is fully faithful.'
 
   - property: preserves finite products
     proof: See <a href="https://mathoverflow.net/questions/386144">MO/386144</a>.
diff --git a/databases/catdat/data/functors/coproduct_sets.yaml b/databases/catdat/data/functors/coproduct_sets.yaml
index 9bf41bc0..a45400c5 100644
--- a/databases/catdat/data/functors/coproduct_sets.yaml
+++ b/databases/catdat/data/functors/coproduct_sets.yaml
@@ -3,7 +3,7 @@ name: binary coproduct functor on sets
 notation: $+$
 source: SetxSet
 target: Set
-description: This functor maps a pair of sets $(X,Y)$ to their coproduct $X + Y$.
+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
 
 tags:
@@ -37,3 +37,6 @@ unsatisfied_properties:
 
   - property: essentially injective
     proof: Both $(1,0)$ and $(0,1)$ are mapped to $1$.
+
+  - property: reflector
+    proof: 'Its right adjoint, the diagonal functor $\Delta : X \to X \times X$, is faithful, but not full.'
diff --git a/databases/catdat/data/functors/enveloping_group.yaml b/databases/catdat/data/functors/enveloping_group.yaml
index c54b6236..05451be8 100644
--- a/databases/catdat/data/functors/enveloping_group.yaml
+++ b/databases/catdat/data/functors/enveloping_group.yaml
@@ -14,11 +14,8 @@ related_functors:
   - free_group
 
 satisfied_properties:
-  - property: left adjoint
-    proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \to \Mon$.'
-
-  - property: right-invertible
-    proof: 'In fact, the counit of the adjunction $F \circ U_{\Grp,\Mon} \to \id_{\Grp}$ is an isomorphism since the right adjoint $U_{\Grp,\Mon}$ is fully faithful (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
+  - property: reflector
+    proof: 'By definition, this functor is left adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \hookrightarrow \Mon$, which is fully faithful.'
 
   - property: preserves finite products
     proof: >-
diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml
index 2d987131..08fde8e2 100644
--- a/databases/catdat/data/functors/forget_topology.yaml
+++ b/databases/catdat/data/functors/forget_topology.yaml
@@ -13,19 +13,19 @@ tags:
 
 related_functors: []
 
+comments:
+  - This functor has exactly two right inverses (up to isomorphism), see <a href="https://math.stackexchange.com/questions/4368730" target="_blank">MSE/4368730</a>.
+
 satisfied_properties:
   - property: faithful
     proof: This is trivial.
 
+  - property: reflector
+    proof: 'The indiscrete topology defines a fully faithful functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.'
+
   - property: representable
     proof: This functor is represented by the singleton space.
 
-  - property: right-invertible
-    proof: 'The functor $D : \Set \to \Top$ that endows a set with the discrete topology provides a right inverse. Remark: Another right inverse functor can be defined with the indiscrete topology. These are the only right inverses (up to isomorphism) by <a href="https://math.stackexchange.com/questions/4368730" target="_blank">MSE/4368730</a>.'
-
-  - property: left adjoint
-    proof: 'The indiscrete topology defines a functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.'
-
 unsatisfied_properties:
   - property: essentially injective
     proof: This is trivial.
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index b77bf4a1..fcbfb8ae 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -15,6 +15,7 @@
 	"essentially injective": false,
 	"left-invertible": false,
 	"right-invertible": false,
+	"reflector": false,
 
 	"cofinitary": true,
 	"conservative": true,
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index 9ade56ee..b9897d75 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -31,5 +31,6 @@
 	"preserves coreflexive equalizers": true,
 	"essentially injective": true,
 	"left-invertible": true,
-	"right-invertible": true
+	"right-invertible": true,
+	"reflector": true
 }

From f5a79b5a6f813cdc64b40aca110763d079e66954 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 00:32:26 +0200
Subject: [PATCH 08/13] add property: is a coreflector

---
 .../catdat/data/functor-properties/coreflector.yaml      | 9 +++++++++
 databases/catdat/data/functor-properties/reflector.yaml  | 2 +-
 databases/catdat/data/functors/forget_topology.yaml      | 3 +++
 databases/catdat/data/functors/group_units.yaml          | 7 ++-----
 databases/catdat/data/functors/product_sets.yaml         | 5 ++++-
 .../catdat/scripts/expected-data/forget_vector.json      | 1 +
 databases/catdat/scripts/expected-data/id_Set.json       | 3 ++-
 7 files changed, 22 insertions(+), 8 deletions(-)
 create mode 100644 databases/catdat/data/functor-properties/coreflector.yaml

diff --git a/databases/catdat/data/functor-properties/coreflector.yaml b/databases/catdat/data/functor-properties/coreflector.yaml
new file mode 100644
index 00000000..113cabf7
--- /dev/null
+++ b/databases/catdat/data/functor-properties/coreflector.yaml
@@ -0,0 +1,9 @@
+id: coreflector
+relation: is a
+description: 'A functor $F : \C \to \D$ is a <i>coreflector</i> if it is right adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full coreflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\eta : \id_{\D} \to F \circ G$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
+nlab_link: https://ncatlab.org/nlab/show/coreflective+subcategory
+invariant_under_equivalences: true
+dual_property: reflector
+related_properties:
+  - right adjoint
+  - right-invertible
diff --git a/databases/catdat/data/functor-properties/reflector.yaml b/databases/catdat/data/functor-properties/reflector.yaml
index 55a9fc8b..f631e50a 100644
--- a/databases/catdat/data/functor-properties/reflector.yaml
+++ b/databases/catdat/data/functor-properties/reflector.yaml
@@ -3,7 +3,7 @@ relation: is a
 description: 'A functor $F : \C \to \D$ is a <i>reflector</i> if it is left adjoint to a functor $G : \D \to \C$ which is fully faithful. Hence, $G$ is equivalent to the inclusion of a full reflective subcategory. The condition that $G$ is fully faithful can also be expressed by the condition that the counit $\varepsilon : F \circ G \to \id_{\D}$ is an isomorphism (Prop. 3.4 at the <a href="https://ncatlab.org/nlab/show/adjoint+functor#FullyFaithfulAndInvertibleAdjoints" target="_blank">nLab</a>).'
 nlab_link: https://ncatlab.org/nlab/show/reflective+subcategory
 invariant_under_equivalences: true
-# dual_property: null FIXME
+dual_property: coreflector
 related_properties:
   - left adjoint
   - right-invertible
diff --git a/databases/catdat/data/functors/forget_topology.yaml b/databases/catdat/data/functors/forget_topology.yaml
index 08fde8e2..97a31425 100644
--- a/databases/catdat/data/functors/forget_topology.yaml
+++ b/databases/catdat/data/functors/forget_topology.yaml
@@ -23,6 +23,9 @@ satisfied_properties:
   - property: reflector
     proof: 'The indiscrete topology defines a fully faithful functor $I : \Set \to \Top$ which is right adjoint to $U_{\Top}$.'
 
+  - property: coreflector
+    proof: 'The discrete topology defines a fully faithful functor $D : \Set \to \Top$ which is left adjoint to $U_{\Top}$.'
+
   - property: representable
     proof: This functor is represented by the singleton space.
 
diff --git a/databases/catdat/data/functors/group_units.yaml b/databases/catdat/data/functors/group_units.yaml
index cd0ad5e4..8a7d05ae 100644
--- a/databases/catdat/data/functors/group_units.yaml
+++ b/databases/catdat/data/functors/group_units.yaml
@@ -13,11 +13,8 @@ tags:
 related_functors: []
 
 satisfied_properties:
-  - property: right-invertible
-    proof: The forgetful functor provides a right inverse, since the group of units of a group $G$ is isomorphic to $G$.
-
-  - property: right adjoint
-    proof: This functor is right adjoint to the forgetful functor $\Grp \to \Mon$.
+  - property: coreflector
+    proof: 'This functor is right adjoint to the forgetful functor $U_{\Grp,\Mon} : \Grp \hookrightarrow \Mon$, which is fully faithful.'
 
   - property: finitary
     proof: 'There is a direct way to prove this, but here is an abstract argument: Since the forgetful functor $\Grp \to \Set$ is conservative and finitary, it suffices to prove that the composition $\Mon \to \Set$, which maps a monoid to its set of units, is finitary. This functor is represented by the monoid $\langle x,y : xy = yx = 1 \rangle \cong \IZ$. It has a finite presentation and hence is finitely presentable in the categorical sense (Corollary 3.13 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>).'
diff --git a/databases/catdat/data/functors/product_sets.yaml b/databases/catdat/data/functors/product_sets.yaml
index 9e32c27d..5de7318c 100644
--- a/databases/catdat/data/functors/product_sets.yaml
+++ b/databases/catdat/data/functors/product_sets.yaml
@@ -3,7 +3,7 @@ name: binary product functor on sets
 notation: $\times$
 source: SetxSet
 target: Set
-description: This functor maps a pair of sets $(X,Y)$ to their product $X \times Y$.
+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
 
@@ -47,3 +47,6 @@ unsatisfied_properties:
 
   - property: preserves coequalizers
     proof: 'Since the diagonal functor $\Delta : \Set \to \Set \times \Set$ preserves coequalizers (in fact, all colimits), it would follow that the composition $\Set \to \Set$, $X \mapsto X^2$ preserves coequalizers. But this is the <a href="/functor/squaring_sets">squaring functor</a>, from we already know that it does not preserve coequalizers.'
+
+  - property: coreflector
+    proof: 'Its left adjoint, the diagonal functor $\Delta : X \to X \times X$, is faithful, but not full.'
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index fcbfb8ae..c64b5367 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -16,6 +16,7 @@
 	"left-invertible": false,
 	"right-invertible": false,
 	"reflector": false,
+	"coreflector": false,
 
 	"cofinitary": true,
 	"conservative": true,
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index b9897d75..28508338 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -32,5 +32,6 @@
 	"essentially injective": true,
 	"left-invertible": true,
 	"right-invertible": true,
-	"reflector": true
+	"reflector": true,
+	"coreflector": true
 }

From 4f53202e1f66bc6349cbea35e626f1ecfa48066c Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Wed, 17 Jun 2026 23:50:45 +0200
Subject: [PATCH 09/13] add criterion for zero preserving functors

---
 .../functor-implications/limits preservation.yaml   | 13 +++++++++++++
 databases/catdat/data/functors/forget_abelian.yaml  |  3 ---
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml
index ee9b91ea..baf7a714 100644
--- a/databases/catdat/data/functor-implications/limits preservation.yaml	
+++ b/databases/catdat/data/functor-implications/limits preservation.yaml	
@@ -132,3 +132,16 @@
     - preserves monomorphisms
   proof: Any monomorphism in the domain is a regular monomorphism and is mapped to a regular monomorphism.
   is_equivalence: false
+
+- id: zero_preserving_condition
+  assumptions:
+    - preserves terminal objects
+  mapped_assumptions:
+    source:
+      - pointed
+    target:
+      - pointed
+  conclusions:
+    - preserves initial objects
+  proof: This is trivial.
+  is_equivalence: false
diff --git a/databases/catdat/data/functors/forget_abelian.yaml b/databases/catdat/data/functors/forget_abelian.yaml
index 92a87387..4b8ca4bb 100644
--- a/databases/catdat/data/functors/forget_abelian.yaml
+++ b/databases/catdat/data/functors/forget_abelian.yaml
@@ -25,9 +25,6 @@ satisfied_properties:
   - property: left-invertible
     proof: The abelianization functor $\Grp \to \Ab$, $G \mapsto G^{\ab}$ provides a left inverse.
 
-  - property: preserves initial objects
-    proof: The trivial group is initial in both $\Ab$ and $\Grp$.
-
   - property: preserves coequalizers
     proof: 'This follows from the concrete construction of coequalizers, but it can also be proven as follows: Assume that $f,g : A \rightrightarrows B$ have coequalizer $p : B \to C$ in $\Ab$. If $G$ is any group and $h : B \to G$ is a homomorphism with $hf = hg$, consider the image factorization $h = i h''$ of $h$. We have $h'' f = h'' g$, and the image $\im(h)$ is abelian. Hence, there is a unique homomorphism $k : C \to \im(h)$ with $kp = h''$. Hence, $ik : C \to G$ satisfies $ikp = h$. Uniqueness follows since we already know that the forgetful functor is preserves epimorphisms.'
 

From 936b6b0106cd38a837a09d13a412fabccf8f3350 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 00:11:17 +0200
Subject: [PATCH 10/13] add the forgetful functor Grp ---> Set_*

---
 .../catdat/data/functors/forget_group.yaml    |  1 +
 .../data/functors/forget_group_pointed.yaml   | 44 +++++++++++++++++++
 .../catdat/data/functors/forget_inverses.yaml |  2 +
 3 files changed, 47 insertions(+)
 create mode 100644 databases/catdat/data/functors/forget_group_pointed.yaml

diff --git a/databases/catdat/data/functors/forget_group.yaml b/databases/catdat/data/functors/forget_group.yaml
index 312a9cf5..605349e4 100644
--- a/databases/catdat/data/functors/forget_group.yaml
+++ b/databases/catdat/data/functors/forget_group.yaml
@@ -15,6 +15,7 @@ related_functors:
   - forget_vector
   - forget_ring
   - forget_abelian
+  - forget_group_pointed
 
 satisfied_properties:
   - property: representable
diff --git a/databases/catdat/data/functors/forget_group_pointed.yaml b/databases/catdat/data/functors/forget_group_pointed.yaml
new file mode 100644
index 00000000..711dd788
--- /dev/null
+++ b/databases/catdat/data/functors/forget_group_pointed.yaml
@@ -0,0 +1,44 @@
+id: forget_group_pointed
+name: forgetful functor from groups to pointed sets
+notation: $U_{\Grp,\Set_*}$
+source: Grp
+target: 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
+
+tags:
+  - algebra
+  - forgetful
+
+related_functors:
+  - forget_group
+  - forget_inverses
+
+satisfied_properties:
+  - property: right adjoint
+    proof: A left adjoint can be constructed by mapping a pointed set $(X,x_0)$ to the free group $F(X)$ modulo $x_0 = 1$.
+
+  - property: conservative
+    proof: 'We already know that the forgetful functor $U_{\Grp} : \Grp \to \Set$ is conservative.'
+
+  - property: finitary
+    proof: 'Since the forgetful functor $U_{\Set_*} : \Set_* \to \Set$ is finitary and conservative, it suffices to prove that the composition $U_{\Set_*} \circ U_{\Grp,\Set_*} : \Grp \to \Set_*$ is finitary. This is just the forgetful functor $U_{\Grp} : \Grp \to \Set$ and therefore finitary.'
+
+  - property: preserves reflexive coequalizers
+    proof: 'It suffices to prove that $U_{\Grp} : \Grp \to \Set$ preserves them, which follows from Theorem 2.5 at the <a href="https://ncatlab.org/nlab/show/reflexive+coequalizer" target="_blank">nLab</a>.'
+
+  - property: preserves epimorphisms
+    proof: This follows from the classifications of epimorphisms in <a href="/category/Grp">$\Grp$</a> and in <a href="/category/Set*">$\Set_*$</a>.
+
+  - property: essentially surjective
+    proof: Let $(X,x_0)$ be a pointed set. If $X$ is finite, we can endow $X$ with a cyclic group structure in which $x_0$ is the identity element. If $X$ is infinite, there is a bijection between $X$ and the set $P_{<\aleph_0}(X)$ of finite subsets of $X$, and we may assume that $x_0$ is mapped to $\varnothing$. Since $P_{<\aleph_0}(X)$ carries a group structure with identity element $\varnothing$ (it is the underlying set of $\IF_2^{\oplus X}$), it follows that $X$ also carries a group structure with identity element $x_0$.
+
+unsatisfied_properties:
+  - property: essentially injective
+    proof: This is trivial.
+
+  - property: preserves coequalizers
+    proof: 'The coequalizer of $1,2 : \IZ \rightrightarrows \IZ$ is the trivial group in $\Grp$, but the coequalizer of these maps in $\Set_*$ is infinite.'
+
+  - property: right-invertible
+    proof: 'Assume that there is a functor $G : \Set_* \to \Grp$ with $U \circ G \cong \id_{\Set_*}$, where $U : \Grp \to \Set_*$ is the forgetful functor. By using transport of structure, we can even assume that $U \circ G = \id_{\Set_*}$. Consider the set $X = \{x_0,x_1,x_2\}$ and the pointed set $(X,x_0)$. It carries a group structure with identity element $x_0$ such that every pointed map $(X,x_0) \to (X,x_0)$ is a group homomorphism (namely, its image under $G$). A group of order $3$ is isomorphic to $C_3$. If $t$ is a generator of $C_3$, then the map $U(C_3) \to U(C_3)$, $1 \mapsto 1$, $t \mapsto t$, $t^2 \mapsto t$ is pointed, but not a group homomorphism.'
diff --git a/databases/catdat/data/functors/forget_inverses.yaml b/databases/catdat/data/functors/forget_inverses.yaml
index b96f8acf..2b208d6e 100644
--- a/databases/catdat/data/functors/forget_inverses.yaml
+++ b/databases/catdat/data/functors/forget_inverses.yaml
@@ -12,7 +12,9 @@ tags:
   - forgetful
 
 related_functors:
+  - forget_group
   - forget_abelian
+  - forget_group_pointed
 
 satisfied_properties:
   - property: full

From 7d422e26bf33f380977c1c17efd82a89a61f5b7c Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 04:51:07 +0200
Subject: [PATCH 11/13] add property: lifts small (co)limits

---
 .../functor-implications/equivalences.yaml    |  2 +-
 .../limits preservation.yaml                  | 22 +++++++++++++++++++
 .../data/functor-implications/monadic.yaml    |  8 +++++++
 .../data/functor-properties/cocontinuous.yaml |  1 +
 .../data/functor-properties/continuous.yaml   |  1 +
 .../lifts small colimits.yaml                 |  8 +++++++
 .../lifts small limits.yaml                   |  8 +++++++
 .../scripts/expected-data/forget_vector.json  |  4 +++-
 .../catdat/scripts/expected-data/id_Set.json  |  4 +++-
 src/lib/server/transforms.ts                  | 15 +++++++++++++
 10 files changed, 70 insertions(+), 3 deletions(-)
 create mode 100644 databases/catdat/data/functor-properties/lifts small colimits.yaml
 create mode 100644 databases/catdat/data/functor-properties/lifts small limits.yaml

diff --git a/databases/catdat/data/functor-implications/equivalences.yaml b/databases/catdat/data/functor-implications/equivalences.yaml
index 84dd3892..14c00525 100644
--- a/databases/catdat/data/functor-implications/equivalences.yaml
+++ b/databases/catdat/data/functor-implications/equivalences.yaml
@@ -19,7 +19,7 @@
     Hence, $R$ (and $L$) are (pseudo-)inverse to $F$.
   is_equivalence: true
 
-- id: equivalence_monadic
+- id: equivalence_consequences
   assumptions:
     - equivalence
   conclusions:
diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml
index baf7a714..03dddfef 100644
--- a/databases/catdat/data/functor-implications/limits preservation.yaml	
+++ b/databases/catdat/data/functor-implications/limits preservation.yaml	
@@ -145,3 +145,25 @@
     - preserves initial objects
   proof: This is trivial.
   is_equivalence: false
+
+- id: lift_implies_preservation
+  assumptions:
+    - lifts small limits
+  mapped_assumptions:
+    target:
+      - complete
+  conclusions:
+    - continuous
+  proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram. Since $\D$ is complete, the diagram $F \circ X$ has a limit cone. Since $F$ lifts small limits, there is a limit cone of $X$ which is mapped by $F$ to the limit cone of $F \circ X$. Hence, $F$ preserves this limit cone of $X$. Since any other limit cone of $X$ is isomorphic to it, the claim follows.'
+  is_equivalence: false
+
+- id: preservation_implies_lift
+  assumptions:
+    - continuous
+  mapped_assumptions:
+    source:
+      - complete
+  conclusions:
+    - lifts small limits
+  proof: 'Let $F : \C \to \D$ be the given functor and $X : \I \to \C$ be a small diagram such that $F \circ X$ has a limit cone. By assumption, $X$ has a limit cone, and $F$ maps it to a limit cone of $F \circ X$. But then the image must be isomorphic to the given limit cone.'
+  is_equivalence: false
diff --git a/databases/catdat/data/functor-implications/monadic.yaml b/databases/catdat/data/functor-implications/monadic.yaml
index e10fe05e..8de8f0fe 100644
--- a/databases/catdat/data/functor-implications/monadic.yaml
+++ b/databases/catdat/data/functor-implications/monadic.yaml
@@ -20,3 +20,11 @@
     - monadic
   proof: This is the crude monadicity theorem. A proof can be found in <a href="https://ncatlab.org/nlab/show/Sheaves+in+Geometry+and+Logic" target="_blank">Mac Lane & Moerdijk</a>, Thm. IV.4.2.
   is_equivalence: false
+
+- id: monadic_lift_limits
+  assumptions:
+    - monadic
+  conclusions:
+    - lifts small limits
+  proof: 'See <a href="https://ncatlab.org/nlab/show/Abstract+and+Concrete+Categories" target="_blank">Joy of Cats</a>, Prop. 20.12.'
+  is_equivalence: false
diff --git a/databases/catdat/data/functor-properties/cocontinuous.yaml b/databases/catdat/data/functor-properties/cocontinuous.yaml
index 54ea6f3e..5eee49fa 100644
--- a/databases/catdat/data/functor-properties/cocontinuous.yaml
+++ b/databases/catdat/data/functor-properties/cocontinuous.yaml
@@ -10,3 +10,4 @@ related_properties:
   - left adjoint
   - preserves coequalizers
   - finitary
+  - lifts small colimits
diff --git a/databases/catdat/data/functor-properties/continuous.yaml b/databases/catdat/data/functor-properties/continuous.yaml
index 4739d6cf..2f2cca28 100644
--- a/databases/catdat/data/functor-properties/continuous.yaml
+++ b/databases/catdat/data/functor-properties/continuous.yaml
@@ -10,3 +10,4 @@ related_properties:
   - right adjoint
   - preserves equalizers
   - cofinitary
+  - lifts small limits
diff --git a/databases/catdat/data/functor-properties/lifts small colimits.yaml b/databases/catdat/data/functor-properties/lifts small colimits.yaml
new file mode 100644
index 00000000..5464f27d
--- /dev/null
+++ b/databases/catdat/data/functor-properties/lifts small colimits.yaml	
@@ -0,0 +1,8 @@
+id: lifts small colimits
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>lifts small colimits</i> when for every small diagram $X : \I \to \C$ and every every colimit cocone of $F \circ X$ there is a colimit cocone of $X$ that is mapped by $F$ to the given colimit cocone of $F \circ X$.'
+nlab_link: https://ncatlab.org/nlab/show/lifted+limit
+invariant_under_equivalences: true
+dual_property: lifts small limits
+related_properties:
+  - cocontinuous
diff --git a/databases/catdat/data/functor-properties/lifts small limits.yaml b/databases/catdat/data/functor-properties/lifts small limits.yaml
new file mode 100644
index 00000000..e8db2f74
--- /dev/null
+++ b/databases/catdat/data/functor-properties/lifts small limits.yaml	
@@ -0,0 +1,8 @@
+id: lifts small limits
+relation: ''
+description: 'A functor $F : \C \to \D$ <i>lifts small limits</i> when for every small diagram $X : \I \to \C$ and every every limit cone of $F \circ X$ there is a limit cone of $X$ that is mapped by $F$ to the given limit cone of $F \circ X$.'
+nlab_link: https://ncatlab.org/nlab/show/lifted+limit
+invariant_under_equivalences: true
+dual_property: lifts small colimits
+related_properties:
+  - continuous
diff --git a/databases/catdat/scripts/expected-data/forget_vector.json b/databases/catdat/scripts/expected-data/forget_vector.json
index c64b5367..c2733e69 100644
--- a/databases/catdat/scripts/expected-data/forget_vector.json
+++ b/databases/catdat/scripts/expected-data/forget_vector.json
@@ -17,6 +17,7 @@
 	"right-invertible": false,
 	"reflector": false,
 	"coreflector": false,
+	"lifts small colimits": false,
 
 	"cofinitary": true,
 	"conservative": true,
@@ -34,5 +35,6 @@
 	"right adjoint": true,
 	"preserves terminal objects": true,
 	"preserves reflexive coequalizers": true,
-	"preserves coreflexive equalizers": true
+	"preserves coreflexive equalizers": true,
+	"lifts small limits": true
 }
diff --git a/databases/catdat/scripts/expected-data/id_Set.json b/databases/catdat/scripts/expected-data/id_Set.json
index 28508338..8cebd163 100644
--- a/databases/catdat/scripts/expected-data/id_Set.json
+++ b/databases/catdat/scripts/expected-data/id_Set.json
@@ -33,5 +33,7 @@
 	"left-invertible": true,
 	"right-invertible": true,
 	"reflector": true,
-	"coreflector": true
+	"coreflector": true,
+	"lifts small limits": true,
+	"lifts small colimits": true
 }
diff --git a/src/lib/server/transforms.ts b/src/lib/server/transforms.ts
index fa5685ba..b42098fc 100644
--- a/src/lib/server/transforms.ts
+++ b/src/lib/server/transforms.ts
@@ -49,6 +49,21 @@ export function display_property_assignment(
 		}
 	}
 
+	// TODO: improve this
+	if (
+		property.is_satisfied === 0 &&
+		property.id.startsWith('lifts') &&
+		!property.relation
+	) {
+		return {
+			id: property.id,
+			label: property.id.replace(/^lifts/, 'lift'),
+			proof: property.proof,
+			is_deduced: Boolean(property.is_deduced),
+			relation: 'does not',
+		}
+	}
+
 	if (property.is_satisfied === 0) {
 		property.relation = relation_negations[property.relation]
 	}

From 63f6e9ed40058e09b64481379a01b8f2838369da Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 04:57:41 +0200
Subject: [PATCH 12/13] add result on additive functors

---
 .../functor-implications/limits preservation.yaml   | 13 +++++++++++++
 databases/catdat/data/functors/p-torsion.yaml       |  3 ---
 databases/catdat/data/functors/torsion.yaml         |  6 +-----
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/databases/catdat/data/functor-implications/limits preservation.yaml b/databases/catdat/data/functor-implications/limits preservation.yaml
index 03dddfef..60d46af6 100644
--- a/databases/catdat/data/functor-implications/limits preservation.yaml	
+++ b/databases/catdat/data/functor-implications/limits preservation.yaml	
@@ -146,6 +146,19 @@
   proof: This is trivial.
   is_equivalence: false
 
+- id: biproduct_preserving_condition
+  assumptions:
+    - preserves finite products
+  mapped_assumptions:
+    source:
+      - biproducts
+    target:
+      - biproducts
+  conclusions:
+    - preserves finite coproducts
+  proof: This is trivial.
+  is_equivalence: false
+
 - id: lift_implies_preservation
   assumptions:
     - lifts small limits
diff --git a/databases/catdat/data/functors/p-torsion.yaml b/databases/catdat/data/functors/p-torsion.yaml
index a719682b..3b114583 100644
--- a/databases/catdat/data/functors/p-torsion.yaml
+++ b/databases/catdat/data/functors/p-torsion.yaml
@@ -20,9 +20,6 @@ satisfied_properties:
   - property: right adjoint
     proof: 'This functor is clearly right adjoint to $A \mapsto A/pA$.'
 
-  - property: preserves coproducts
-    proof: This is easy to check using the description of coproducts as direct sums.
-
   - property: finitary
     proof: >-
       This follows abstractly from the fact that $\IZ/p$ is finitely presentable. We nevertheless give a direct proof. Let $(A_i)$ be a filtered diagram of abelian groups. We need to show that the canonical map
diff --git a/databases/catdat/data/functors/torsion.yaml b/databases/catdat/data/functors/torsion.yaml
index 289a7e4d..9a27dea2 100644
--- a/databases/catdat/data/functors/torsion.yaml
+++ b/databases/catdat/data/functors/torsion.yaml
@@ -14,12 +14,8 @@ related_functors:
   - p-torsion
 
 satisfied_properties:
-  - property: preserves coproducts
-    proof: This is easy to check using the description of coproducts as direct sums.
-
   - property: preserves finite products
-    # TODO: automate this with an implication
-    proof: Finite products coincide with finite direct sums.
+    proof: This is easy.
 
   - property: preserves equalizers
     proof: 'Let $E \subseteq A$ be the equalizer of two homomorphisms $f,g : A \rightrightarrows B$. If $a \in T(A)$ is equalized by $T(f),T(g) : T(A) \rightrightarrows T(B)$, then $a \in A$ is equalized by $f,g$, so that $a \in E$. It follows $a \in T(A) \cap E = T(E)$.'

From 9265e4ba97597cc648fb59730c975f863766cf38 Mon Sep 17 00:00:00 2001
From: Script Raccoon <scriptraccoon@gmail.com>
Date: Thu, 18 Jun 2026 05:39:07 +0200
Subject: [PATCH 13/13] add indiscrete topology functor Set ---> Top

---
 .../data/functors/discrete_topology.yaml      |  3 +-
 .../data/functors/indiscrete_topology.yaml    | 40 +++++++++++++++++++
 2 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 databases/catdat/data/functors/indiscrete_topology.yaml

diff --git a/databases/catdat/data/functors/discrete_topology.yaml b/databases/catdat/data/functors/discrete_topology.yaml
index c58f9b30..62746944 100644
--- a/databases/catdat/data/functors/discrete_topology.yaml
+++ b/databases/catdat/data/functors/discrete_topology.yaml
@@ -10,7 +10,8 @@ tags:
   - topology
   - free
 
-related_functors: []
+related_functors:
+  - indiscrete_topology
 
 satisfied_properties:
   - property: left adjoint
diff --git a/databases/catdat/data/functors/indiscrete_topology.yaml b/databases/catdat/data/functors/indiscrete_topology.yaml
new file mode 100644
index 00000000..93b2d381
--- /dev/null
+++ b/databases/catdat/data/functors/indiscrete_topology.yaml
@@ -0,0 +1,40 @@
+id: indiscrete_topology
+name: indiscrete topology functor
+notation: $I$
+source: Set
+target: 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
+
+tags:
+  - topology
+
+related_functors:
+  - discrete_topology
+
+satisfied_properties:
+  - property: full
+    proof: This is trivial.
+
+  - property: preserves initial objects
+    proof: This is obvious.
+
+  - property: right adjoint
+    proof: 'This functor is right adjoint to the forgetful functor $U_{\Top} : \Top \to \Set$.'
+
+  - property: left-invertible
+    proof: The forgetful functor provides a left inverse.
+
+  - property: preserves coequalizers
+    proof: 'This follows easily from the description of coequalizers in $\Set$ and $\Top$, and the fact that if $p : X \to Y$ is a surjective map, then $I(p) : I(X) \to I(Y)$ is a quotient map.'
+
+  - property: finitary
+    proof: >-
+      Let $X$ be a filtered diagram of sets. We need to prove that the filtered colimit of spaces $\colim_i I(X_i)$ is indiscrete. If $X_i$ is empty for all $i$, this is trivial. Otherwise, by considering a slice of the index category, we may assume that every $X_i$ is non-empty. A topological space $Y$ is indiscrete iff there are at most two continuous maps $Y \to S$, where $S$ is the Sierpinski space; there are exactly two when $Y$ is non-empty. We have
+      $$\textstyle \Hom(\colim_i I(X_i),S) \cong \lim_i \Hom(I(X_i),S) \cong \lim_i \{\varnothing, X_i\}.$$
+      For every $i \to j$ the map $I(X_i) \to I(X_j)$ pulls back $\varnothing \mapsto \varnothing$ and $X_j \mapsto X_i$. Thus, the limit has exactly two elements.
+
+unsatisfied_properties:
+  - property: preserves finite coproducts
+    proof: If $X$ and $Y$ are two non-empty sets, the canonical continuous bijection $I(X) + I(Y) \to I(X + Y)$ is not an isomorphism since $I(X) + I(Y)$ is not indiscrete as witnessed by the open subset $X$.