diff --git a/databases/catdat/data/001_categories/008_tiny.sql b/databases/catdat/data/001_categories/008_tiny.sql index 3121d4b3..d8c315ec 100644 --- a/databases/catdat/data/001_categories/008_tiny.sql +++ b/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 idempotent morphism 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$.
The walking splitting can be interpreted as a skeleton of the category of $\mathbb{F}_2$-vector spaces of dimension $\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 9b6a96ca..21c01c84 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/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'); \ No newline at end of file +('walking_span', 'walking_pair'), +('walking_splitting', 'walking_idempotent'), +('walking_splitting', 'walking_isomorphism'); \ 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 60b66093..7d24b734 100644 --- a/databases/catdat/data/001_categories/200_category-tags.sql +++ b/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'), diff --git a/databases/catdat/data/003_category-property-assignments/walking_splitting.sql b/databases/catdat/data/003_category-property-assignments/walking_splitting.sql new file mode 100644 index 00000000..5e934e2e --- /dev/null +++ b/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.
+ 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.
+ 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 [AR01, Lemma 3.3] 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.' +); \ 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 809a8680..f1e0a2a4 100644 --- a/databases/catdat/data/005_special-objects/002_initial_objects.sql +++ b/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$'); diff --git a/databases/catdat/data/005_special-objects/003_terminal_objects.sql b/databases/catdat/data/005_special-objects/003_terminal_objects.sql index ea7e846b..adda66c1 100644 --- a/databases/catdat/data/005_special-objects/003_terminal_objects.sql +++ b/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$'); diff --git a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql index 5cac6ec0..188e440f 100644 --- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql +++ b/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', diff --git a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql index fcf8ecfd..e77f9e1c 100644 --- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql +++ b/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', diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql index 0e00d7b5..61840503 100644 --- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql +++ b/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', 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 1e86ca29..39d6e992 100644 --- a/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql +++ b/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 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 67d65d61..30f36531 100644 --- a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql +++ b/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',