From 0eecd5d48538b824e316056b5a276f21e6f07686 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Fri, 3 Jul 2026 18:40:47 -0400 Subject: [PATCH 1/2] Add Sierpinski topos (category of set functions and commutative squares) --- databases/catdat/data/categories/Set.yaml | 1 + .../catdat/data/categories/Set_arrow.yaml | 66 +++++++++++++++++++ databases/catdat/data/categories/SetxSet.yaml | 1 + databases/catdat/data/categories/Sh(X).yaml | 1 + 4 files changed, 69 insertions(+) create mode 100644 databases/catdat/data/categories/Set_arrow.yaml diff --git a/databases/catdat/data/categories/Set.yaml b/databases/catdat/data/categories/Set.yaml index 96acaef92..12b34127a 100644 --- a/databases/catdat/data/categories/Set.yaml +++ b/databases/catdat/data/categories/Set.yaml @@ -17,6 +17,7 @@ related_categories: - Set_f - SetxSet - Setne + - Set_arrow satisfied_properties: - property: locally small diff --git a/databases/catdat/data/categories/Set_arrow.yaml b/databases/catdat/data/categories/Set_arrow.yaml new file mode 100644 index 000000000..d3a4aee38 --- /dev/null +++ b/databases/catdat/data/categories/Set_arrow.yaml @@ -0,0 +1,66 @@ +id: Set_arrow +name: category of set functions and commutative squares +notation: $\Set^{\rightarrow}$ +objects: >- + triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \to Y$ is a function +morphisms: >- + a morphism $(X, Y, f) \to (X', Y', f')$ is a pair of functions $\ell : X \to X'$ and $r : Y \to Y'$ making a commutative square, i.e. such that $f' \circ \ell = r \circ f$ +description: This category is also known as the Sierpinski topos, since it is equivalent to the category of sheaves on the Sierpinski space. +nlab_link: https://ncatlab.org/nlab/show/Sierpinski+topos + +tags: + - set theory + +related_categories: + - Set + - SetxSet + - Sh(X) + +satisfied_properties: + - property: locally small + proof: This is easy. + + - property: semi-strongly connected + proof: >- + Consider two objects $(X, Y, f)$ and $(X', Y', f')$. If $X'$ is non-empty with element $x'$, we can construct a morphism $(\ell, r) : (X, Y, f) \to (X', Y', f')$ where $\ell$ is the constant function with value $x'$, and $r$ is the constant function with value $f'(x')$; and similarly if $X$ is non-empty we can construct a morphism $(X', Y', f') \to (X, Y, f)$. Otherwise, if $X$ and $Y$ are both empty, we can reduce to the fact that $\Set$ is semi-strongly connected to find $r$ in one direction, and fill in $\ell$ as the unique function $\varnothing \to \varnothing$. + + - property: Grothendieck topos + proof: It is equivalent to the category of presheaves on the walking morphism $I$. + + - property: locally strongly finitely presentable + proof: It is equivalent to the category of models of the algebraic theory with two sorts, and a single unary operation from one sort to the other. + +unsatisfied_properties: + - property: skeletal + proof: 'Consider $\id_X : X \to X$ and $\id_Y : Y \to Y$ for isomorphic but non-equal sets $X$ and $Y$.' + + - property: generator + proof: >- + Suppose $\Set^{\rightarrow}$ had a generator. Then by this result, every subterminal object would be either initial or terminal. However, in fact, $0 \to 1$ is a subterminal object which is isomorphic to neither the initial object $0 \to 0$ nor the terminal object $1 \to 1$. + +special_objects: + initial object: + description: the unique function $0 \to 0$ + terminal object: + description: the unique function $1 \to 1$ + coproducts: + description: component-wise defined disjoint union, equipped with the disjoint union of the functions + products: + description: component-wise defined cartesian product, equipped with the product function + +special_morphisms: + isomorphisms: + description: pairs $(\ell, r)$ where $\ell$ and $r$ are both bijections + proof: This is easy. + monomorphisms: + description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective + proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and similarly, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$. + epimorphisms: + description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective + proof: For the non-trivial direction, use the fact that the category is regular and epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise. + regular monomorphisms: + description: same as monomorphisms + proof: This is because the category is mono-regular. + regular epimorphisms: + description: same as epimorphisms + proof: This is because the category is epi-regular. diff --git a/databases/catdat/data/categories/SetxSet.yaml b/databases/catdat/data/categories/SetxSet.yaml index e16932f75..a8d324b53 100644 --- a/databases/catdat/data/categories/SetxSet.yaml +++ b/databases/catdat/data/categories/SetxSet.yaml @@ -11,6 +11,7 @@ tags: related_categories: - Set + - Set_arrow - Sh(X) satisfied_properties: diff --git a/databases/catdat/data/categories/Sh(X).yaml b/databases/catdat/data/categories/Sh(X).yaml index 75c56ed19..e5459ab9c 100644 --- a/databases/catdat/data/categories/Sh(X).yaml +++ b/databases/catdat/data/categories/Sh(X).yaml @@ -13,6 +13,7 @@ tags: related_categories: - Set - SetxSet + - Set_arrow - Sh(X,Ab) comments: From fb40d6e7a241e69eb4b47cc04c57f7daf47f563a Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sat, 4 Jul 2026 08:56:21 +0200 Subject: [PATCH 2/2] small adjustments for Set_arrow --- databases/catdat/data/categories/Set_arrow.yaml | 17 +++++++++++------ databases/catdat/data/macros.yaml | 1 + 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/databases/catdat/data/categories/Set_arrow.yaml b/databases/catdat/data/categories/Set_arrow.yaml index d3a4aee38..3a9c2d791 100644 --- a/databases/catdat/data/categories/Set_arrow.yaml +++ b/databases/catdat/data/categories/Set_arrow.yaml @@ -4,8 +4,13 @@ notation: $\Set^{\rightarrow}$ objects: >- triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \to Y$ is a function morphisms: >- - a morphism $(X, Y, f) \to (X', Y', f')$ is a pair of functions $\ell : X \to X'$ and $r : Y \to Y'$ making a commutative square, i.e. such that $f' \circ \ell = r \circ f$ -description: This category is also known as the Sierpinski topos, since it is equivalent to the category of sheaves on the Sierpinski space. + a morphism $(X, Y, f) \to (X', Y', f')$ is a pair of functions $\ell : X \to X'$ and $r : Y \to Y'$ making a commutative square + $$\begin{CD} + X @>{f}>> Y \\ + @V{\ell}VV @VV{r}V \\ + X' @>>{f'}> Y' + \end{CD}$$ +description: This category is an example of the arrow category $\Arr(\C)$, where $\C$ is the category of sets. It is also known as the Sierpinski topos, since it is equivalent to the category of sheaves on the Sierpinski space. nlab_link: https://ncatlab.org/nlab/show/Sierpinski+topos tags: @@ -22,10 +27,10 @@ satisfied_properties: - property: semi-strongly connected proof: >- - Consider two objects $(X, Y, f)$ and $(X', Y', f')$. If $X'$ is non-empty with element $x'$, we can construct a morphism $(\ell, r) : (X, Y, f) \to (X', Y', f')$ where $\ell$ is the constant function with value $x'$, and $r$ is the constant function with value $f'(x')$; and similarly if $X$ is non-empty we can construct a morphism $(X', Y', f') \to (X, Y, f)$. Otherwise, if $X$ and $Y$ are both empty, we can reduce to the fact that $\Set$ is semi-strongly connected to find $r$ in one direction, and fill in $\ell$ as the unique function $\varnothing \to \varnothing$. + Consider two objects $(X, Y, f)$ and $(X', Y', f')$. If $X'$ is non-empty with element $x'$, we can construct a morphism $(\ell, r) : (X, Y, f) \to (X', Y', f')$ where $\ell$ is the constant function with value $x'$, and $r$ is the constant function with value $f'(x')$; and similarly if $X$ is non-empty we can construct a morphism $(X', Y', f') \to (X, Y, f)$. Otherwise, if $X$ and $X'$ are both empty, we can reduce to the fact that $\Set$ is semi-strongly connected to find $r$ in one direction, and fill in $\ell$ as the unique function $\varnothing \to \varnothing$. - property: Grothendieck topos - proof: It is equivalent to the category of presheaves on the walking morphism $I$. + proof: It is equivalent to the category of presheaves on the walking morphism. - property: locally strongly finitely presentable proof: It is equivalent to the category of models of the algebraic theory with two sorts, and a single unary operation from one sort to the other. @@ -54,10 +59,10 @@ special_morphisms: proof: This is easy. monomorphisms: description: pairs $(\ell, r)$ where $\ell$ and $r$ are both injective - proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and similarly, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$. + proof: For the non-trivial direction, use the fact that the domain functor taking an object $(X, Y, f)$ to $X$ and a morphism $(\ell, r)$ to $\ell$ is representable by $1 \to 1$; and moreover, the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \to 1$. epimorphisms: description: pairs $(\ell, r)$ where $\ell$ and $r$ are both surjective - proof: For the non-trivial direction, use the fact that the category is regular and epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise. + proof: For the non-trivial direction, use the fact that the category is epi-regular, so any epimorphism is a coequalizer; and the fact that coequalizers can be calculated component-wise. regular monomorphisms: description: same as monomorphisms proof: This is because the category is mono-regular. diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index ef3c6a26e..844eb0443 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -121,3 +121,4 @@ \Isom: \mathbf{Isom} \Pair: \mathbf{Pair} \Span: \mathbf{Span} +\Arr: \mathbf{Arr}