From 6531cf1a31477c3c8e3d083ebf27f5231634fd6d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 26 Apr 2026 10:59:11 +0200 Subject: [PATCH 1/7] add the walking reflexive pair --- databases/catdat/data/001_categories/008_tiny.sql | 10 ++++++++++ .../data/001_categories/100_related-categories.sql | 6 +++++- .../catdat/data/001_categories/200_category-tags.sql | 2 ++ .../data/006_special-morphisms/002_isomorphisms.sql | 5 +++++ .../data/006_special-morphisms/003_monomorphisms.sql | 5 +++++ .../data/006_special-morphisms/004_epimorphisms.sql | 5 +++++ 6 files changed, 32 insertions(+), 1 deletion(-) diff --git a/databases/catdat/data/001_categories/008_tiny.sql b/databases/catdat/data/001_categories/008_tiny.sql index d8c315ec..d0921351 100644 --- a/databases/catdat/data/001_categories/008_tiny.sql +++ b/databases/catdat/data/001_categories/008_tiny.sql @@ -130,4 +130,14 @@ VALUES 'This category could also be called the "walking split idempotent" (or "walking section", "walking retraction"), but we chose a name that emphasizes that the splitting belongs to the data. Notice that the $5$ given morphisms are indeed closed under composition. For example, $p \circ ip = p$ and $ip \circ i = i$.
The walking splitting can be interpreted as a skeleton of the category of $\mathbb{F}_2$-vector spaces of dimension $\leq 1$.', NULL, NULL +), +( + 'walking_reflexive_pair', + 'walking reflexive pair', + '$\mathrm{Refl}$', + 'two objects $0$ and $1$', + 'the identities, morphisms $p,q : 1 \rightrightarrows 0$, a morphism $i : 0 \to 1$ with $p i = q i = \mathrm{id}_0$, and the two idempotent morphisms $ip, iq : 1 \to 1$.', + 'The mentioned morphisms are indeed closed under composition, for example $ip \circ iq = iq$ and $iq \circ ip = ip$. The name of this category comes from the fact that a functor out of it is the same as an reflexive pair in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.', + NULL, + NULL ); \ No newline at end of file diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql index 21c01c84..8d89be25 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/databases/catdat/data/001_categories/100_related-categories.sql @@ -158,7 +158,11 @@ VALUES ('walking_morphism', 'walking_splitting'), ('walking_pair', 'walking_morphism'), ('walking_pair', 'walking_fork'), +('walking_pair', 'walking_reflexive_pair'), +('walking_reflexive_pair', 'walking_pair'), +('walking_reflexive_pair', 'walking_splitting'), ('walking_span', 'walking_morphism'), ('walking_span', 'walking_pair'), ('walking_splitting', 'walking_idempotent'), -('walking_splitting', 'walking_isomorphism'); \ No newline at end of file +('walking_splitting', 'walking_isomorphism'), +('walking_splitting', 'walking_reflexive_pair'); \ No newline at end of file diff --git a/databases/catdat/data/001_categories/200_category-tags.sql b/databases/catdat/data/001_categories/200_category-tags.sql index 7d24b734..dad838db 100644 --- a/databases/catdat/data/001_categories/200_category-tags.sql +++ b/databases/catdat/data/001_categories/200_category-tags.sql @@ -108,6 +108,8 @@ VALUES ('walking_morphism', 'thin'), ('walking_pair', 'finite'), ('walking_pair', 'category theory'), +('walking_reflexive_pair', 'finite'), +('walking_reflexive_pair', 'category theory'), ('walking_span', 'finite'), ('walking_span', 'category theory'), ('walking_span', 'thin'), diff --git a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql index 188e440f..f8e2b8d5 100644 --- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql @@ -350,6 +350,11 @@ VALUES 'the two identities', 'This is trivial.' ), +( + 'walking_reflexive_pair', + 'the two identities', + 'This is obvious.' +), ( 'walking_span', 'the three identities', diff --git a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql index e77f9e1c..2405ca5c 100644 --- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql @@ -340,6 +340,11 @@ VALUES 'every morphism', 'This is trivial.' ), +( + 'walking_reflexive_pair', + 'the identities and $i$', + 'Since $pi = \mathrm{id}$, but $ip \neq \mathrm{id}$, we conclude that $i$ is a monomorphism, but $p$ is not. Likewise, $q$ is no monomorphism. Then $ip$ and $iq$ cannot be monomorphisms either.' +), ( 'walking_span', 'every morphism', diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql index 61840503..08d6a1d2 100644 --- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql @@ -326,6 +326,11 @@ VALUES 'every morphism', 'Each $0 \to 1$ is an epimorphism since the only morphism starting at $1$ is the identity.' ), +( + 'walking_reflexive_pair', + 'the identities, $p$, $q$', + 'Since $pi = \mathrm{id}$, but $ip \neq \mathrm{id}$, we conclude that $p$ is an epimorphism, but $i$ is not. Likewise, $q$ is an epimorphism. Since $i$ is not an epimorphism, $ip$ and $iq$ are no epimorphisms either.' +), ( 'walking_span', 'every morphism', From 08e2e75e5bffac2bdd0157e60ea8ec22a604cbad Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 26 Apr 2026 11:34:41 +0200 Subject: [PATCH 2/7] add diagram --- databases/catdat/data/001_categories/008_tiny.sql | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/databases/catdat/data/001_categories/008_tiny.sql b/databases/catdat/data/001_categories/008_tiny.sql index d0921351..104888e7 100644 --- a/databases/catdat/data/001_categories/008_tiny.sql +++ b/databases/catdat/data/001_categories/008_tiny.sql @@ -136,8 +136,10 @@ VALUES 'walking reflexive pair', '$\mathrm{Refl}$', 'two objects $0$ and $1$', - 'the identities, morphisms $p,q : 1 \rightrightarrows 0$, a morphism $i : 0 \to 1$ with $p i = q i = \mathrm{id}_0$, and the two idempotent morphisms $ip, iq : 1 \to 1$.', - 'The mentioned morphisms are indeed closed under composition, for example $ip \circ iq = iq$ and $iq \circ ip = ip$. The name of this category comes from the fact that a functor out of it is the same as an reflexive pair in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.', + 'the identities, a morphism $i : 0 \to 1$, morphisms $p,q : 1 \rightrightarrows 0$ with $p i = q i = \mathrm{id}_0$, and the two idempotent morphisms $ip, iq : 1 \to 1$.', + 'The mentioned morphisms are indeed closed under composition, for example $ip \circ iq = iq$ and $iq \circ ip = ip$. + $$0 \begin{array}{c} \xtwoheadleftarrow{~~p~~} \\ \xhookrightarrow{~~i~~} \\ \xtwoheadleftarrow{~~q~~} \end{array} 1$$ + The name of this category comes from the fact that a functor out of it is the same as an reflexive pair in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.', NULL, NULL ); \ No newline at end of file From afd2eb7d72ceddcbdae9c2fb3693e87b73aaecbf Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 26 Apr 2026 11:36:25 +0200 Subject: [PATCH 3/7] add related category --- databases/catdat/data/001_categories/100_related-categories.sql | 1 + 1 file changed, 1 insertion(+) diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql index 8d89be25..a56ce7bf 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/databases/catdat/data/001_categories/100_related-categories.sql @@ -161,6 +161,7 @@ VALUES ('walking_pair', 'walking_reflexive_pair'), ('walking_reflexive_pair', 'walking_pair'), ('walking_reflexive_pair', 'walking_splitting'), +('walking_reflexive_pair', 'Delta'), ('walking_span', 'walking_morphism'), ('walking_span', 'walking_pair'), ('walking_splitting', 'walking_idempotent'), From 2182ffb2d0cc30c742ed5acc899040464459a2d3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 26 Apr 2026 12:20:16 +0200 Subject: [PATCH 4/7] assign most properties to the walking reflexive pair --- .../walking_reflexive_pair.sql | 81 +++++++++++++++++++ .../002_initial_objects.sql | 1 + .../005_regular-monomorphisms.sql | 5 ++ .../006_regular-epimorphisms.sql | 5 ++ 4 files changed, 92 insertions(+) create mode 100644 databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql diff --git a/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql b/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql new file mode 100644 index 00000000..f8ade454 --- /dev/null +++ b/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql @@ -0,0 +1,81 @@ +INSERT INTO category_property_assignments ( + category_id, + property_id, + is_satisfied, + reason +) +VALUES +( + 'walking_reflexive_pair', + 'finite', + TRUE, + 'This is trivial.' +), +( + 'walking_reflexive_pair', + 'small', + TRUE, + 'This is trivial.' +), +( + 'walking_reflexive_pair', + 'strongly connected', + TRUE, + 'This is trivial.' +), +( + 'walking_reflexive_pair', + 'gaunt', + TRUE, + 'This is obvious.' +), +( + 'walking_reflexive_pair', + 'initial object', + TRUE, + 'The object $0$ is clearly an initial object.' +), +( + 'walking_reflexive_pair', + 'mono-regular', + TRUE, + 'The only non-identity monomorphism is $i$, which is the equalizer of $\mathrm{id}_1, ip : 1 \rightrightarrows 1$ (since $pi = \mathrm{id}_0$).' +), +( + 'walking_reflexive_pair', + 'epi-regular', + TRUE, + 'The only non-identity epimorphisms are $p$ and $q$. The morphism $p$ is the coequalizer of $\mathrm{id}_1, ip : 1 \rightrightarrows 1$ (since $pi = \mathrm{id}_0$), and for $q$ it is the same argument.' +), +( + 'walking_reflexive_pair', + 'equalizers', + TRUE, + 'There are four non-equal parallel pairs: $(p,q)$, $(ip,iq)$, $(\mathrm{id}_1,ip)$, and $(\mathrm{id}_1,iq)$. The first two have the same equalizer (if it exists) since $i$ is a monomorphism, and the last two are symmetric. So it suffices to consider $(p,q)$ and $(\mathrm{id}_1,ip)$.
+ (1) We claim that $i$ is an equalizer of $p,q$. We have $pi = qi$ since both sides are just $\mathrm{id}_0$. Conversely, let $f : x \to 1$ be a morphism with $pf = qf$, we will show that $f$ factors through $i$. If $x = 0$, so that $f = i$, we are done. If $x=1$, then there are three possibilities. The first one is $f=\mathrm{id}_1$, which violates $pf = qf$. The other two are $f = ip, iq$, which indeed factor through $i$.
+ (2) We already know that $i$ is an equalizer of $(\mathrm{id}_1,ip)$ (since $pi = \mathrm{id}_0$).' +), +( + 'walking_reflexive_pair', + 'strict initial object', + FALSE, + 'The morphism $p : 1 \to 0$ is a witness.' +), +( + 'walking_reflexive_pair', + 'filtered', + FALSE, + 'The morphisms $p,q : 1 \rightrightarrows 0$ are not coequalized by any morphism since $\mathrm{id}_0 \, p \neq \mathrm{id}_0 \, q$ and $i p \neq i q$.' +), +( + 'walking_reflexive_pair', + 'reflexive coequalizers', + FALSE, + 'The reflexive pair $p,q : 1 \rightrightarrows 0$ has no coequalizer, in fact is not coequalized by any morphism since $\mathrm{id}_0 \, p \neq \mathrm{id}_0 \, q$ and $i p \neq i q$.' +), +( + 'walking_reflexive_pair', + 'pullbacks', + FALSE, + 'The morphisms $p,q : 1 \rightrightarrows 0$ have no pullback: otherwise, since $0$ is initial, they would be coequalized by some morphism. But this is not the case since $\mathrm{id}_0 \, p \neq \mathrm{id}_0 \, q$ and $i p \neq i q$.' +); \ No newline at end of file diff --git a/databases/catdat/data/005_special-objects/002_initial_objects.sql b/databases/catdat/data/005_special-objects/002_initial_objects.sql index f1e0a2a4..55f6058d 100644 --- a/databases/catdat/data/005_special-objects/002_initial_objects.sql +++ b/databases/catdat/data/005_special-objects/002_initial_objects.sql @@ -59,6 +59,7 @@ VALUES ('walking_isomorphism', 'both objects'), ('walking_fork', '$0$'), ('walking_morphism', '$0$'), +('walking_reflexive_pair', '$0$'), ('walking_span', '$0$'), ('walking_splitting', '$0$'), ('Z', 'constant functor with value $\varnothing$'), diff --git a/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql b/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql index 39d6e992..bb328fb2 100644 --- a/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql @@ -280,6 +280,11 @@ VALUES 'same as isomorphisms', 'This is because the category is right cancellative.' ), +( + 'walking_reflexive_pair', + 'same as monomorphisms', + 'This is because the category is mono-regular.' +), ( 'walking_span', 'same as isomorphisms', diff --git a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql index 30f36531..884addf6 100644 --- a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql @@ -275,6 +275,11 @@ VALUES 'same as isomorphisms', 'This is because the category is left cancellative.' ), +( + 'walking_reflexive_pair', + 'same as epimorphisms', + 'This is because the category is epi-regular.' +), ( 'walking_span', 'same as isomorphisms', From c45fc467b9512cfe12458f363e454666b95a0b42 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Apr 2026 04:39:54 +0200 Subject: [PATCH 5/7] fix typo --- databases/catdat/data/001_categories/008_tiny.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/databases/catdat/data/001_categories/008_tiny.sql b/databases/catdat/data/001_categories/008_tiny.sql index 104888e7..a7371149 100644 --- a/databases/catdat/data/001_categories/008_tiny.sql +++ b/databases/catdat/data/001_categories/008_tiny.sql @@ -139,7 +139,7 @@ VALUES 'the identities, a morphism $i : 0 \to 1$, morphisms $p,q : 1 \rightrightarrows 0$ with $p i = q i = \mathrm{id}_0$, and the two idempotent morphisms $ip, iq : 1 \to 1$.', 'The mentioned morphisms are indeed closed under composition, for example $ip \circ iq = iq$ and $iq \circ ip = ip$. $$0 \begin{array}{c} \xtwoheadleftarrow{~~p~~} \\ \xhookrightarrow{~~i~~} \\ \xtwoheadleftarrow{~~q~~} \end{array} 1$$ - The name of this category comes from the fact that a functor out of it is the same as an reflexive pair in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.', + The name of this category comes from the fact that a functor out of it is the same as a reflexive pair in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.', NULL, NULL ); \ No newline at end of file From db349d1b96ea414d1aee002e6c5d5c93ceffe9e4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Apr 2026 05:01:20 +0200 Subject: [PATCH 6/7] add back: finite + cauchy complete => filtered colimits this was already in the database, but then was "improved" to => finitely accessible, which however is not dualized, since we do not have finitely coaccessible. --- .../001_limits-colimits-existence-implications.sql | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql index a29adac7..60316fc4 100644 --- a/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql +++ b/databases/catdat/data/004_category-implications/001_limits-colimits-existence-implications.sql @@ -181,6 +181,15 @@ VALUES ), ( 'finite_filtered_colimits', + -- TODO: remove this once "finitely coaccessible" is added, + -- because only then the result "finite_accessible" is dualized + '["essentially finite", "Cauchy complete"]', + '["filtered colimits"]', + 'See MO/509853.', + FALSE +), +( + 'finite_accessible', '["essentially finite", "Cauchy complete"]', '["finitely accessible"]', 'See MO/509853, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.', From 0dbb5b1046a2933ec5749174803e9bb982a78fb2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Apr 2026 05:26:38 +0200 Subject: [PATCH 7/7] walking reflexive pair has generators and cogenerators --- .../walking_reflexive_pair.sql | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql b/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql index f8ade454..2b1d0ec7 100644 --- a/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql +++ b/databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql @@ -55,6 +55,18 @@ VALUES (1) We claim that $i$ is an equalizer of $p,q$. We have $pi = qi$ since both sides are just $\mathrm{id}_0$. Conversely, let $f : x \to 1$ be a morphism with $pf = qf$, we will show that $f$ factors through $i$. If $x = 0$, so that $f = i$, we are done. If $x=1$, then there are three possibilities. The first one is $f=\mathrm{id}_1$, which violates $pf = qf$. The other two are $f = ip, iq$, which indeed factor through $i$.
(2) We already know that $i$ is an equalizer of $(\mathrm{id}_1,ip)$ (since $pi = \mathrm{id}_0$).' ), +( + 'walking_reflexive_pair', + 'generator', + TRUE, + 'The object $1$ is a generator: $0$ is the only other object and any two morphisms with domain $0$ are equal.' +), +( + 'walking_reflexive_pair', + 'cogenerator', + TRUE, + 'The object $1$ is a cogenerator: $0$ is the only other object and the only non-equal pair of morphisms with codomain $0$ is $p,q$, which also satisfies $ip \neq iq$. Remark: Also $0$ is a cogenerator.' +), ( 'walking_reflexive_pair', 'strict initial object',