Add the walking reflexive pair

databases/catdat/data/001_categories/008_tiny.sql

@@ -130,4 +130,16 @@ 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$.<br>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, 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 a <a href="https://ncatlab.org/nlab/show/reflexive+pair" target="_blank">reflexive pair</a> in the target category. Notice that its dual (the walking coreflexive pair) is just the truncated simplex category $\Delta^{\leq 1}$.',
+	NULL,
+	NULL
 );

databases/catdat/data/001_categories/100_related-categories.sql

@@ -158,7 +158,12 @@ 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_reflexive_pair', 'Delta'),
 ('walking_span', 'walking_morphism'),
 ('walking_span', 'walking_pair'),
 ('walking_splitting', 'walking_idempotent'),
-('walking_splitting', 'walking_isomorphism');
+('walking_splitting', 'walking_isomorphism'),
+('walking_splitting', 'walking_reflexive_pair');

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'),

databases/catdat/data/003_category-property-assignments/walking_reflexive_pair.sql

@@ -0,0 +1,93 @@
+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)$.<br>
+	(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$.<br>
+	(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',
+	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$.'
+);

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 <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>.',
+	FALSE
+),
+(
+	'finite_accessible',
 	'["essentially finite", "Cauchy complete"]',
 	'["finitely accessible"]',
 	'See <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.',

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$'),

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',

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',

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',

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',

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',