diff --git a/databases/catdat/data/categories/Set.yaml b/databases/catdat/data/categories/Set.yaml index 96acaef9..12b34127 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 00000000..3a9c2d79 --- /dev/null +++ b/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 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: + - 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 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. + +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 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. diff --git a/databases/catdat/data/categories/SetxSet.yaml b/databases/catdat/data/categories/SetxSet.yaml index e16932f7..a8d324b5 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 75c56ed1..e5459ab9 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: diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index ef3c6a26..844eb044 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}