Add Sierpinski topos (category of set functions and commutative squares)

databases/catdat/data/categories/Set.yaml

@@ -17,6 +17,7 @@ related_categories:
   - Set_f
   - SetxSet
   - Setne
+  - Set_arrow
 
 satisfied_properties:
   - property: locally small

databases/catdat/data/categories/Set_arrow.yaml

@@ -0,0 +1,71 @@
+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
+  $$\begin{CD}
+  X @>{f}>> Y \\
+  @V{\ell}VV @VV{r}V \\
+  X' @>>{f'}> Y'
+  \end{CD}$$
+description: This category is an example of the <a href="https://ncatlab.org/nlab/show/arrow+category" target="_blank">arrow category</a> $\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:
+  - 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 $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 <a href="/category/walking_morphism">the walking morphism</a>.
+
+  - 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 <a href="/content/topos-with-generator">this result</a>, 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 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 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.

databases/catdat/data/categories/SetxSet.yaml

@@ -11,6 +11,7 @@ tags:
 
 related_categories:
   - Set
+  - Set_arrow
   - Sh(X)
 
 satisfied_properties:

databases/catdat/data/categories/Sh(X).yaml

@@ -13,6 +13,7 @@ tags:
 related_categories:
   - Set
   - SetxSet
+  - Set_arrow
   - Sh(X,Ab)
 
 comments:

databases/catdat/data/macros.yaml

@@ -121,3 +121,4 @@
 \Isom: \mathbf{Isom}
 \Pair: \mathbf{Pair}
 \Span: \mathbf{Span}
+\Arr: \mathbf{Arr}