Add the walking splitting

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

@@ -120,4 +120,14 @@ VALUES
 	'The name of this category comes from the fact that a functor out of it is the same as an <a href="https://ncatlab.org/nlab/show/idempotent" target="_blank">idempotent morphism</a> in the target category. It can also be seen as the delooping of the monoid $\{1,e\}$ in which $e^2=e$.',
 	NULL,
 	NULL
+),
+(
+	'walking_splitting',
+	'walking splitting',
+	'$\mathrm{Split}$',
+	'two objects $0$ and $1$',
+	'the identities, morphisms $i : 0 \to 1$, $p : 1 \to 0$ satisfying $pi = \mathrm{id}_0$, and the idempotent $ip : 1 \to 1$.',
+	'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
 );

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

@@ -145,6 +145,7 @@ VALUES
 ('walking_idempotent', 'walking_morphism'),
 ('walking_idempotent', 'walking_isomorphism'),
 ('walking_idempotent', 'BG_f'),
+('walking_idempotent', 'walking_splitting'),
 ('walking_isomorphism', '1'),
 ('walking_isomorphism', 'walking_morphism'),
 ('walking_isomorphism', 'walking_idempotent'),
@@ -154,7 +155,10 @@ VALUES
 ('walking_morphism', 'walking_composable_pair'),
 ('walking_morphism', 'walking_span'),
 ('walking_morphism', 'walking_idempotent'),
+('walking_morphism', 'walking_splitting'),
 ('walking_pair', 'walking_morphism'),
 ('walking_pair', 'walking_fork'),
 ('walking_span', 'walking_morphism'),
-('walking_span', 'walking_pair');
+('walking_span', 'walking_pair'),
+('walking_splitting', 'walking_idempotent'),
+('walking_splitting', 'walking_isomorphism');

databases/catdat/data/001_categories/200_category-tags.sql

@@ -111,6 +111,8 @@ VALUES
 ('walking_span', 'finite'),
 ('walking_span', 'category theory'),
 ('walking_span', 'thin'),
+('walking_splitting', 'finite'),
+('walking_splitting', 'category theory'),
 ('Z', 'algebraic geometry'),
 ('Z', 'category theory'),
 ('Z_div', 'number theory'),

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

@@ -0,0 +1,87 @@
+INSERT INTO category_property_assignments (
+	category_id,
+	property_id,
+	is_satisfied,
+	reason
+)
+VALUES
+(
+	'walking_splitting',
+	'finite',
+	TRUE,
+	'This is trivial.'
+),
+(
+	'walking_splitting',
+	'small',
+	TRUE,
+	'This is trivial.'
+),
+(
+	'walking_splitting',
+	'gaunt',
+	TRUE,
+	'This is obvious.'
+),
+(
+	'walking_splitting',
+	'pointed',
+	TRUE,
+	'The object $0$ is initial and terminal. This also means that $\mathrm{id}_0, i, p, ip$ are zero morphisms. The only non-zero morphism is $\mathrm{id}_1$.'
+),
+(
+	'walking_splitting',
+	'equalizers',
+	TRUE,
+	'The only parallel pair of non-equal morphisms is $\mathrm{id}_1, ip : 1 \rightrightarrows 1$, and their equalizer is $i$.'
+),
+(
+	'walking_splitting',
+	'self-dual',
+	TRUE,
+	'There is an isomorphism $\mathrm{Split}^\mathrm{op} \to \mathrm{Split}$ defined by $0 \mapsto 0$, $1 \mapsto 1$, $i \mapsto p$, $p \mapsto i$.'
+),
+(
+	'walking_splitting',
+	'normal',
+	TRUE,
+	'The only non-identity monomorphism is $i : 0 \to 1$, which is the kernel of $\mathrm{id}_1$.'
+),
+(
+	'walking_splitting',
+	'generator',
+	TRUE,
+	'The object $1$ a generator, since the only parallel pair of non-equal morphisms is $\mathrm{id}_1, ip : 1 \rightrightarrows 1$ with domain $1$.'
+),
+(
+	'walking_splitting',
+	'preadditive',
+	TRUE,
+	'We can define $\mathrm{id}_1 + \mathrm{id}_1 := ip$ (and it is clear how to add zero morphisms) and then verify that the axioms of a preadditive category hold. Alternatively, it suffices to find a preadditive category which is isomorphic to the walking splitting: Consider the full subcategory of $\mathbf{Vect}_{\mathbb{F}_2}$ that consists only of the trivial vector space $\{0\}$ and $\mathbb{F}_2$. Since $\mathbf{Vect}_{\mathbb{F}_2}$ is preadditive, it is preadditive as well. It has two objects, two identities, the morphisms $i : \{0\} \to \mathbb{F}_2$, $p : \mathbb{F}_2 \to \{0\}$, and the zero morphism $ip : \mathbb{F}_2 \to \mathbb{F}_2$. Clearly, $pi$ is the identity.'
+),
+(
+	'walking_splitting',
+	'sifted colimits',
+	TRUE,
+	'We work with the representation of the category as $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2}$, the category of vector spaces over $\mathbb{F}_2$ of dimension $\leq 1$. It suffices to show that it is closed under sifted colimits in $\mathbf{Vect}_{\mathbb{F}_2}$. More generally, we show this for $\mathbf{Vect}^{\leq d}_K \subseteq \mathbf{Vect}_K$, where $d \in \mathbb{N}$ and $K$ is a field. So let  $X : \mathcal{I} \to \mathbf{Vect}_K$ be a sifted diagram with colimit $(u_i : X_i \to X_\infty)_{i \in \mathcal{I}}$. Since $\mathcal{I}$ is sifted, for finitely many objects $i_1,\dotsc,i_n \in \mathcal{I}$ there is an object $k$ that admits morphisms $i_1 \to k, \dotsc, i_n \to k$; this is all we need to know about $\mathcal{I}$. Assume that each $X_i$ is of dimension $\leq d$, we need to show this for $X_\infty$ as well.<br>
+	Every element in $X_\infty$ is a finite sum of elements of the form $u_i(x_i)$ with $x_i \in X_i$. Choose an object $k$ with morphisms $i \to k$ for every occurring $i$. If $y_i \in X_k$ denotes the image of $x_i$, we get $\sum_i u_i(x_i) = \sum_i u_k(y_i) = u_k(\sum_i y_i)$. Therefore, every element of $X_\infty$ has the form $u_i(x_i)$ for some $i \in \mathcal{I}$ and $x_i \in X_i$. Moreover, for finitely many elements in $X_\infty$ the index $i$ may be chosen uniformly.<br>
+	Now, if $X_\infty$ has dimension $> d$, it would have linearly independent vectors $v_0,\dotsc,v_d$, all of which have a preimage in $X_i$ for some $i \in \mathcal{I}$. But then these preimages would be linearly independent as well, which contradicts $\dim(X_i) \leq d$.'
+),
+(
+	'walking_splitting',
+	'generalized variety',
+	TRUE,
+	'Again we work with $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2}$. We already know that it has sifted colimits and that the embedding to $\mathbf{Vect}_{\mathbb{F}_2}$ preserves them. The object $0$ is initial and hence strongly finitely presentable. The object $\mathbb{F}_2$ is strongly finitely presentable in $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2}$ since its hom-functor is the composition of the embedding and the forgetful functor $\mathbf{Vect}_{\mathbb{F}_2} \to \mathbf{Set}$, and the latter preserves sifted colimits by <a href="http://www.tac.mta.ca/tac/volumes/8/n3/8-03abs.html" target="_blank">[AR01, Lemma 3.3]</a> applied to $\mathbb{F}_2 \in \mathbf{Vect}_{\mathbb{F}_2}$.'
+),
+(
+	'walking_splitting',
+	'filtered-colimit-stable monomorphisms',
+	TRUE,
+	'We saw above that the embedding $\mathbf{Vect}^{\leq 1}_{\mathbb{F}_2} \hookrightarrow \mathbf{Vect}_{\mathbb{F}_2}$ is closed under sifted colimits, hence under filtered colimits. Hence, it preserves filtered colimits. Moreover, it preserves and reflects monomorphisms. Therefore, the claim follows from $\mathbf{Vect}_{\mathbb{F}_2}$.'
+),
+(
+	'walking_splitting',
+	'one-way',
+	FALSE,
+	'The morphism $ip : 1 \to 1$ provides a counterexample.'
+);

databases/catdat/data/005_special-objects/002_initial_objects.sql

@@ -60,6 +60,7 @@ VALUES
 ('walking_fork', '$0$'),
 ('walking_morphism', '$0$'),
 ('walking_span', '$0$'),
+('walking_splitting', '$0$'),
 ('Z', 'constant functor with value $\varnothing$'),
 ('Z_div', '$1$'),
 ('walking_composable_pair', '$0$');

databases/catdat/data/005_special-objects/003_terminal_objects.sql

@@ -55,6 +55,7 @@ VALUES
 ('walking_commutative_square', '$d$'),
 ('walking_isomorphism', 'both objects'),
 ('walking_morphism', '$1$'),
+('walking_splitting', '$0$'),
 ('Z', 'constant functor with value $1$'),
 ('Z_div', '$0$'),
 ('walking_composable_pair', '$2$');

databases/catdat/data/006_special-morphisms/002_isomorphisms.sql

@@ -355,6 +355,11 @@ VALUES
 	'the three identities',
 	'This is trivial.'
 ),
+(
+	'walking_splitting',
+	'the two identities',
+	'This is obvious.'
+),
 (
 	'Z',
 	'natural isomorphisms',

databases/catdat/data/006_special-morphisms/003_monomorphisms.sql

@@ -345,6 +345,11 @@ VALUES
 	'every morphism',
 	'It is a thin category.'
 ),
+(
+	'walking_splitting',
+	'the identities and $i$',
+	'The morphism $i$ is even a split monomorphism. The morphism $p$ is not a monomorphism since $p \circ \mathrm{id}_1 = p \circ ip$. The morphism $ip$ is not a monomorphism since it would imply that $p$ is a monomorphism.'
+),
 (
 	'Z',
 	'pointwise injective natural transformations',

databases/catdat/data/006_special-morphisms/004_epimorphisms.sql

@@ -331,6 +331,11 @@ VALUES
 	'every morphism',
 	'It is a thin category.'
 ),
+(
+	'walking_splitting',
+	'the identities and $p$',
+	'The morphism $p$ is even a split monomorphism. The morphism $i$ is not an epimorphism since $\mathrm{id}_1 \circ i = ip \circ i$. The morphism $ip$ is not a epimorphism since it would imply that $i$ is an epimorphism.'
+),
 (
 	'Z',
 	'objectwise surjective natural transformations',

databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql

@@ -284,6 +284,11 @@ VALUES
     'walking_span',
     'same as isomorphisms',
     'This is because the category is right cancellative.'
+),
+(
+    'walking_splitting',
+    'same as monomorphisms',
+    'This is because the category is mono-regular.'
 );
 
 INSERT INTO special_morphisms

databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql

@@ -279,7 +279,12 @@ VALUES
     'walking_span',
     'same as isomorphisms',
     'This is because the category is right cancellative.'
-),  
+),
+(
+    'walking_splitting',
+    'same as epimorphisms',
+    'This is because the category is epi-regular.'
+),
 (
     'Z',
     'same as epimorphisms',