From 0187340f4f0757278e6feafddadeb9873a4dbf05 Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sat, 4 Jul 2026 16:49:15 -0400 Subject: [PATCH 1/2] Add category Mono of injective set functions and commutative squares --- databases/catdat/data/categories/FI.yaml | 1 + databases/catdat/data/categories/Mono.yaml | 184 ++++++++++++++++++ .../catdat/data/categories/Set_arrow.yaml | 1 + databases/catdat/data/macros.yaml | 1 + 4 files changed, 187 insertions(+) create mode 100644 databases/catdat/data/categories/Mono.yaml diff --git a/databases/catdat/data/categories/FI.yaml b/databases/catdat/data/categories/FI.yaml index e8f3eb6af..98d823005 100644 --- a/databases/catdat/data/categories/FI.yaml +++ b/databases/catdat/data/categories/FI.yaml @@ -14,6 +14,7 @@ related_categories: - B - FS - FinSet + - Mono satisfied_properties: - property: locally small diff --git a/databases/catdat/data/categories/Mono.yaml b/databases/catdat/data/categories/Mono.yaml new file mode 100644 index 000000000..feb44e264 --- /dev/null +++ b/databases/catdat/data/categories/Mono.yaml @@ -0,0 +1,184 @@ +id: Mono +name: category of injective set functions and commutative diagrams +notation: $\Mono$ +objects: >- + triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \hookrightarrow Y$ is an injective 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 is the full subcategory of $\Set^{\rightarrow}$ consisting of the injective set functions. It is also equivalent to the category of pairs of a set $X$ and a subset $S \subseteq X$, with morphisms $(X, S) \to (Y, T)$ being the functions $f : X \to Y$ such that $f(S) \subseteq T$. +nlab_link: https://ncatlab.org/nlab/show/Mono + +tags: + - set theory + +related_categories: + - Set_arrow + - FI + +satisfied_properties: + - property: locally small + proof: This is easy. + + - property: semi-strongly connected + proof: This is immediate from the fact that $\Mono$ is a full subcategory of $\Set^{\rightarrow}$, and the latter is semi-strongly connected. + + - property: generator + proof: >- + The object $0 \hookrightarrow 1$ is a generator. This is because it represents the codomain functor taking an object $f : X \hookrightarrow Y$ to $Y$, and taking a morphism $(\ell, r)$ to $r$. That functor is faithful because once $r$ is fixed, $\ell$ is uniquely determined since $f'$ is a monomorphism in $\Set$. + + - property: cogenerator + proof: >- + The object $\{ \top, \bot \} \xhookrightarrow{\id} \{ \top, \bot \}$. To see this, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X, Y, f) \rightrightarrows (X', Y', g)$ such that for every morphism $(\ell', r') : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \})$, $(\ell', r') \circ (\ell_1, r_1) = (\ell', r') \circ (\ell_2, r_2)$. Then morphisms $(X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ are equivalent to functions $Y' \to \{ \top, \bot \}$. Since $\{ \top, \bot \}$ is a cogenerator in $\Set$, this implies $r_1 = r_2$; and since $g$ is a monomorphism in $\Set$, we automatically get $\ell_1 = \ell_2$ as well. + + - property: complete + proof: The component-wise limit of injective functions is again an injective function, and it forms the limit in $\Mono$. + check_redundancy: false + + - property: cocomplete + proof: 'We have that $\Mono$ is a reflective subcategory of $\Set^{\rightarrow}$, with the reflector taking a function $f : X \to Y$ to the inclusion map $\im(f) \hookrightarrow Y$. Therefore, the result follows from the fact that $\Set^{\rightarrow}$ is cocomplete.' + check_redundancy: false + + - property: disjoint coproducts + proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts. + + - property: locally cartesian closed + proof: >- + For this construction, we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Now, for any object $(D, D')$ of $\Mono$, the reflector functor $\Set^{\rightarrow} \to \Mono$ induces a reflector functor of slices $\Set^{\rightarrow} / (D' \hookrightarrow D)$ to $\Mono / (D, D')$. We claim that this reflector preserves binary products, i.e. it transforms pullbacks over $D' \hookrightarrow D$ in $\Set^{\rightarrow}$ to pullbacks over $(D, D')$ in $\Mono$. Thus, suppose we have two objects $f, g$ of $\Set^{\rightarrow}$ with degree morphisms to $D' \hookrightarrow D$: + $$\begin{CD} + X @> \deg_X >> D' @< \deg_Y << Y\\ + @V f VV @VVV @VV g V\\ + Z @>> \deg_Z > D @<< \deg_W < W. + \end{CD}$$ + Then the reflector turns $f$ into $(Z, \im(f))$ and $g$ into $(W, \im(g))$. The pullback in $\Mono$ is $(Z \times_D W, \im(f) \times_{D'} \im(g))$. On the other hand, taking the pullback in $\Set^{\rightarrow}$ first, and then applying the reflector, gives $(Z \times_D W, \im(X \times_{D'} Y \to Z \times_D W))$. Thus, we must show $\im(f) \times_{D'} \im(g) = \im(X \times_{D'} Y \to Z \times_D W)$. + + We easily see that $\im(X \times_{D'} Y \to Z \times_D W) \subseteq \im(f) \times_{D'} \im(g)$ (this is the inclusion that we automatically get from the canonical comparison morphism). Conversely, suppose we have $z\in \im(f)$ and $w\in \im(g)$ with the same degree (which must be in $D'$). Then there exist $x\in X$ such that $f(x) = z$ and $y\in Y$ such that $g(y) = w$. Since $\deg_X(x) = \deg_Z(z) = \deg_W(w) = \deg_Y(y) \in D'$, we have $(x, y) \in X \times_{D'} Y$, and the image of $(x, y)$ in $Z \times_D W$ is exactly $(z, w)$, finishing the proof of the claim. + + Therefore, from Lemma 5 here, we conclude that each slice of $\Mono$ is cartesian closed, i.e. that $\Mono$ is locally cartesian closed. + + - property: regular subobject classifier + proof: 'The object $\{ \top, \bot \} \xhookrightarrow{\id} $\{ \top, \bot \}$ is a regular subobject classifier, with $\top : (1, 1, \id) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ consisting of the maps with image $\top$. This follows from the description of regular monomorphisms below.' + + - property: locally finitely presentable + proof: >- + It is equivalent to the category of models of the finite limit sketch with a single limit cone + $$\begin{CD} + X @> \id >> X \\ + @V \id VV @VV f VV \\ + X @>> f > Y. + \end{CD}$$ + + - property: coregular + proof: >- + For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. It suffices to show regular monomorphisms are stable under pushouts. Thus, suppose we have two morphisms $f : (X, X') \to (Y, Y')$ and $g : (X, X') \to (Z, Z')$ where $f$ is a regular monomorphism, which means $f$ is injective and $X' = f^{-1}(Y')$. Then we can construct a pushout diagram + $$\begin{CD} + (X, X') @> f >> (Y, Y') \\ + @V g VV @VV i_1 VV \\ + (Z, Z') @>> i_2 > ((Y \setminus f(X)) \sqcup Z, i_1(Y') \cup i_2(Z')). + \end{CD}$$ + Here $i_1$ sends $f(x) \mapsto g(x) \in Z$ for $x \in X$, and otherwise it sends $y \mapsto y$ for $y \in Y \setminus f(X)$; and $i_2$ is the inclusion of $Z$. We certainly have $i_2$ is injective; it remains to show $i_2^{-1}(i_1(Y') \cup i_2(Z')) = Z'$. However, we have + $$i_2^{-1}(i_1(Y') \cup i_2(Z')) = i_2^{-1}(i_1(Y')) \cup i_2^{-1}(i_2(Z'))$$ + and obviously $i_2^{-1}(i_2(Z')) = Z'$. Therefore, it suffices to show $i_2^{-1}(i_1(Y')) \subseteq Z'$. Thus, suppose we have $z \in Z$ such that $i_2(z) \in i_1(Y')$. That means there exists $y' \in Y'$ such that $z = i_1(y')$. But in order for $i_1(y')$ to land in the $Z$ portion of $(Y \setminus f(X)) \sqcup Z$, we must have $i_1(y') \in f(X)$. That means there exists $x \in X$ such that $f(x) = y'$; and by the assumption on $f$, in fact $x \in X'$. Therefore, $i_2(g(x)) = i_1(f(x)) = y' = i_2(z)$, so $z = g(x) \in Z'$. + + - property: co-Malcev + proof: >- + For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Thus, suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is surjective. Since $\Set$ is co-Malcev, it follows that $E \simeq X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $r(i_1(x)) = x \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. + + - property: effective cocongruences + proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \to X \sqcup_Y X$.' + +unsatisfied_properties: + - property: skeletal + proof: Consider the objects $X \xhookrightarrow{\id} X$ and $Y \xhookrightarrow{\id} Y$ for isomorphic but non-equal sets $X$ and $Y$. + + - property: balanced + proof: The unique morphism from $0 \hookrightarrow 1$ to $1 \hookrightarrow 1$ is both a monomorphism and an epimorphism, but not an isomorphism (see descriptions below). + + - property: cofiltered-limit-stable epimorphisms + proof: >- + Consider the sequence of epimorphisms + $$\begin{CD} + \IN_{\ge n} @> \id >> \IN_{\ge n} \\ + @V ! VV @VV ! V \\ + 1 @>> \id > 1. + \end{CD}$$ + The limit is + $$\begin{CD} + 0 @> \id >> 0 \\ + @V ! VV @VV ! V \\ + 1 @>> \id > 1 + \end{CD}$$ + which is not an epimorphism. + + - property: Malcev + proof: This is clear since $\Set$ is not Malcev, and it has a left exact embedding in $\Mono$ via the functor sending a set $X$ to $X \xhookrightarrow{\id} X$. + +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 $r$ is an injective function, from which it automatically follows that $\ell$ is also injective + proof: For the non-trivial direction, use the fact that the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \hookrightarrow 1$. + epimorphisms: + description: pairs $(\ell, r)$ where $r$ is a surjective function + proof: >- + Suppose we have a morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ such that $r$ is surjective. To see it is an epimorphism, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X', Y', g) \rightrightarrows (T, U, h)$ such that $(\ell_1, r_1) \circ (\ell, r) = (\ell_2, r_2) \circ (\ell, r)$. Then $r_1 \circ r = r_2 \circ r$ implies $r_1 = r_2$. It automatically follows that $\ell_1 = \ell_2$ since $h$ is a monomorphism in $\Set$. + + Conversely, suppose we have an epimorphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$. Then for any set $T$, the morphisms $(X', Y', g) \to (T, T, \id_T)$ are equivalent to the functions $Y' \to T$; therefore, $r$ is an epimorphism in $\Set$. + regular monomorphisms: + description: >- + pairs $(\ell, r)$ where $r$ is an injective function and moreover the commutative square + $$\begin{CD} + X @> f >> Y \\ + @V \ell VV @VV r V \\ + X' @>> g > Y' + \end{CD}$$ + is in fact a cartesian square + proof: >- + To show any regular monomorphism satisfies this condition, suppose we have an equalizer diagram + $$\begin{CD} + X @> f >> Y \\ + @V \ell VV @VV r V \\ + X' @> g >> Y' \\ + @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\ + X'' @>> h > Y''. + \end{CD}$$ + Without loss of generality, we may assume $f$, $g$, $h$, $\ell$, and $r$ are all inclusion maps. Now suppose we have $y' \in Y'$ which is in the intersection of $X'$ and $Y$. Then $y' \in Y$ implies $r_1(y') = r_2(y')$. Therefore, since $h$ is injective, we can conclude $\ell_1(y') = \ell_2(y')$, so in fact $y' \in X$. This shows $X' \cap Y \subseteq X$; the other inclusion is automatic from the commutativity of the diagram. + + To show any morphism satisfying this condition is a regular monomorphism, we may again assume $f$, $g$, $\ell$, and $r$ are all inclusion maps. We can then construct an equalizer diagram + $$\begin{CD} + X @> f >> Y \\ + @V \ell VV @VV r V \\ + X' @> g >> Y' \\ + @V \chi_X V \top_{X'} V @V \chi_Y V \top_{Y'} V \\ + \{ \top, \bot \} @> \id >> \{ \top, \bot \}. + \end{CD}$$ + Here $\top_{X'}$ represents the constant function on $X'$ with value $\top$, and similarly for $\top_{Y'}$. Here, the assumption $X = X' \cap Y$ is used to establish the commutativity of the characteristic morphism $(\chi_X, \chi_Y) : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$. + regular epimorphisms: + description: pairs $(\ell, r)$ where both $\ell$ and $r$ are surjective functions + proof: >- + To show any regular epimorphism satisfies this condition, suppose we have a parallel pair + $$\begin{CD} + X @> f >> Y \\ + @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\ + X' @> g >> Y'. + \end{CD}$$ + To form the coequalizer in $\Mono$, first we may form the coequalizer in $\Set^{\rightarrow}$, $\coeq(\ell_1, \ell_2) \xrightarrow{\bar g} \coeq(r_1, r_2)$. Note this is not injective in general; however, we may apply the reflector to get the coequalizer $\im(\bar g) \hookrightarrow \coeq(r_1, r_2)$ in $\Mono$. Here, clearly the map $Y' \to \coeq(r_1, r_2)$ is surjective. Likewise, both the functions $X' \to \coeq(\ell_1, \ell_2)$ and $coeq(\ell_1, \ell_2) \to \im(\bar g)$ are surjective, so their composition $X' \to \coeq(\ell_1, \ell_2)$ is surjective as well. + + To show any morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ satisfying this condition is a regular epimorphism, note that the kernel pair of $(\ell, r)$ can be computed component-wise. Therefore, the coequalizer in $\Set^{\rightarrow}$ of this kernel pair is exactly $(X', Y', g)$, so applying the reflector does nothing and $(X', Y', g)$ is also the coequalizer in $\Mono$. diff --git a/databases/catdat/data/categories/Set_arrow.yaml b/databases/catdat/data/categories/Set_arrow.yaml index 3a9c2d791..089f1342f 100644 --- a/databases/catdat/data/categories/Set_arrow.yaml +++ b/databases/catdat/data/categories/Set_arrow.yaml @@ -20,6 +20,7 @@ related_categories: - Set - SetxSet - Sh(X) + - Mono satisfied_properties: - property: locally small diff --git a/databases/catdat/data/macros.yaml b/databases/catdat/data/macros.yaml index 844eb0443..41701714f 100644 --- a/databases/catdat/data/macros.yaml +++ b/databases/catdat/data/macros.yaml @@ -122,3 +122,4 @@ \Pair: \mathbf{Pair} \Span: \mathbf{Span} \Arr: \mathbf{Arr} +\Mono: \mathbf{Mono} From 70411104cb467612d33d2b4c07c49b8897a244fa Mon Sep 17 00:00:00 2001 From: Daniel Schepler Date: Sun, 5 Jul 2026 17:13:21 -0400 Subject: [PATCH 2/2] Rework so the primary representation is a pair of a set and a subset --- databases/catdat/data/categories/Mono.yaml | 130 +++++++++------------ 1 file changed, 52 insertions(+), 78 deletions(-) diff --git a/databases/catdat/data/categories/Mono.yaml b/databases/catdat/data/categories/Mono.yaml index feb44e264..a8d78fe04 100644 --- a/databases/catdat/data/categories/Mono.yaml +++ b/databases/catdat/data/categories/Mono.yaml @@ -1,18 +1,13 @@ id: Mono -name: category of injective set functions and commutative diagrams +name: category of sets with a distinguished subset notation: $\Mono$ objects: >- - triples $(X, Y, f)$ where $X$ and $Y$ are sets, and $f : X \hookrightarrow Y$ is an injective function + pairs $(X, X')$ where $X$ is a set and $X' \subseteq X$ is a subset 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}$$ + a morphism $(X, X') \to (Y, Y')$ is a function $f : X \to Y$ such that $f(X') \subseteq Y'$ description: >- - This is the full subcategory of $\Set^{\rightarrow}$ consisting of the injective set functions. It is also equivalent to the category of pairs of a set $X$ and a subset $S \subseteq X$, with morphisms $(X, S) \to (Y, T)$ being the functions $f : X \to Y$ such that $f(S) \subseteq T$. -nlab_link: https://ncatlab.org/nlab/show/Mono + This is equivalent to the full subcategory of objects $(X, Y, f)$ of $\Set^{\rightarrow}$ where $f : X \to Y$ is an injective function. +nlab_link: https://ncatlab.org/nlab/show/M-category#def tags: - set theory @@ -26,30 +21,34 @@ satisfied_properties: proof: This is easy. - property: semi-strongly connected - proof: This is immediate from the fact that $\Mono$ is a full subcategory of $\Set^{\rightarrow}$, and the latter is semi-strongly connected. + proof: This is immediate from the fact that $\Mono$ is equivalent to a full subcategory of $\Set^{\rightarrow}$, and the latter is semi-strongly connected. - property: generator proof: >- - The object $0 \hookrightarrow 1$ is a generator. This is because it represents the codomain functor taking an object $f : X \hookrightarrow Y$ to $Y$, and taking a morphism $(\ell, r)$ to $r$. That functor is faithful because once $r$ is fixed, $\ell$ is uniquely determined since $f'$ is a monomorphism in $\Set$. + The object $(1, 0)$ is a generator. This is because it represents the functor taking an object $(X, X')$ to $X$, and taking a morphism $f : (X, X') \to (Y, Y')$ to the function $f : X \to Y$. - property: cogenerator proof: >- - The object $\{ \top, \bot \} \xhookrightarrow{\id} \{ \top, \bot \}$. To see this, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X, Y, f) \rightrightarrows (X', Y', g)$ such that for every morphism $(\ell', r') : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \})$, $(\ell', r') \circ (\ell_1, r_1) = (\ell', r') \circ (\ell_2, r_2)$. Then morphisms $(X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ are equivalent to functions $Y' \to \{ \top, \bot \}$. Since $\{ \top, \bot \}$ is a cogenerator in $\Set$, this implies $r_1 = r_2$; and since $g$ is a monomorphism in $\Set$, we automatically get $\ell_1 = \ell_2$ as well. + The object $(\{ \top, \bot \}, \{ \top, \bot \})$ is a cogenerator. To see this, suppose we have two morphisms $f, g : (X, X') \rightrightarrows (Y, Y')$ such that for every morphism $h : (Y, Y') \to (\{\top,\bot\}, \{\top,\bot\})$, $h \circ f = h \circ g$. Then the morphisms $(Y, Y') \to (\{\top,\bot\}, \{\top,\bot\})$ are all functions $Y \to \{\top,\bot\}$. Since $\{ \top, \bot \}$ is a cogenerator in $\Set$, this implies $f = g$. - property: complete - proof: The component-wise limit of injective functions is again an injective function, and it forms the limit in $\Mono$. + proof: >- + The component-wise limit gives a pair of a set and a subset, and this pair forms the limit in $\Mono$. check_redundancy: false - property: cocomplete - proof: 'We have that $\Mono$ is a reflective subcategory of $\Set^{\rightarrow}$, with the reflector taking a function $f : X \to Y$ to the inclusion map $\im(f) \hookrightarrow Y$. Therefore, the result follows from the fact that $\Set^{\rightarrow}$ is cocomplete.' + proof: >- + We have that $\Mono$ is a reflective subcategory of $\Set^{\rightarrow}$, with the reflector taking a function $f : X \to Y$ to the pair $(Y, \im(f))$. Therefore, the result follows from the fact that $\Set^{\rightarrow}$ is cocomplete. + + More concretely, suppose we have a diagram $((X_i, X_i'))_{i \in \I}$, with colimit cone $c_i : X_i \to \colim_{i\in\I} X_i$ in $\Set$. Then the colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} c_i(X_i'))$. check_redundancy: false - property: disjoint coproducts - proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts. + proof: This follows from the fact that coproducts in $\Mono$ can be computed component-wise, along with the fact that $\Set$ has disjoint coproducts. - property: locally cartesian closed proof: >- - For this construction, we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Now, for any object $(D, D')$ of $\Mono$, the reflector functor $\Set^{\rightarrow} \to \Mono$ induces a reflector functor of slices $\Set^{\rightarrow} / (D' \hookrightarrow D)$ to $\Mono / (D, D')$. We claim that this reflector preserves binary products, i.e. it transforms pullbacks over $D' \hookrightarrow D$ in $\Set^{\rightarrow}$ to pullbacks over $(D, D')$ in $\Mono$. Thus, suppose we have two objects $f, g$ of $\Set^{\rightarrow}$ with degree morphisms to $D' \hookrightarrow D$: + For any object $(D, D')$ of $\Mono$, the reflector functor $\Set^{\rightarrow} \to \Mono$ induces a reflector functor of slices $\Set^{\rightarrow} / (D' \hookrightarrow D)$ to $\Mono / (D, D')$. We claim that this reflector preserves binary products, i.e. it transforms pullbacks over $D' \hookrightarrow D$ in $\Set^{\rightarrow}$ to pullbacks over $(D, D')$ in $\Mono$. Thus, suppose we have two objects $f, g$ of $\Set^{\rightarrow}$ with degree morphisms to $D' \hookrightarrow D$: $$\begin{CD} X @> \deg_X >> D' @< \deg_Y << Y\\ @V f VV @VVV @VV g V\\ @@ -62,7 +61,7 @@ satisfied_properties: Therefore, from Lemma 5 here, we conclude that each slice of $\Mono$ is cartesian closed, i.e. that $\Mono$ is locally cartesian closed. - property: regular subobject classifier - proof: 'The object $\{ \top, \bot \} \xhookrightarrow{\id} $\{ \top, \bot \}$ is a regular subobject classifier, with $\top : (1, 1, \id) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$ consisting of the maps with image $\top$. This follows from the description of regular monomorphisms below.' + proof: 'The object $(\{ \top, \bot \}, \{ \top, \bot \})$ is a regular subobject classifier, with $\top : (1, 1) \to (\{ \top, \bot \}, \{ \top, \bot \})$ consisting of the function with image $\top$. This follows from the description of regular monomorphisms below.' - property: locally finitely presentable proof: >- @@ -73,9 +72,13 @@ satisfied_properties: X @>> f > Y. \end{CD}$$ + Alternately, we already know $\Mono$ is cocomplete. We claim that both $(1, 0)$ and $(1, 1)$ are finitely presentable objects of $\Mono$. For the first, $(1, 0)$ represents the forgetful functor $(X, X') \mapsto X$; and this functor has a right adjoint $X \mapsto (X, X)$ so it preserves filtered colimits (in fact all colimits). For the second, $(1, 1)$ represents the functor $(X, X') \mapsto X'$. Now by the previous description of colimits, for a filtered diagram $((X_i, X_i'))_{i\in\I}$, first form the filtered colimit of $X_i$ in $\Set$ with cocone $c_i : X_i \to \colim_{i\in\I} X_i$. Then the filtered colimit in $\Mono$ is $(\colim_{i\in\I} X_i, \bigcup_{i\in\I} c_i(X_i'))$. This makes it easy to see that the canonical function $\colim_{i\in\I} \Hom((1,1), (X_i,X_i')) \to \Hom((1,1), \colim_{i\in\I} (X_i,X_i'))$ is surjective. To see it is injective, use the fact that the unique morphism $(1, 0) \to (1, 1)$ is an epimorphism (see below), and we have already seen that the corresponding function for $(1,0)$ is injective. + + Therefore, any finite coproduct of $(1, 0)$ and $(1, 1)$ is finitely presentable; this means any object of the form $([n], [m])$ with $m, n \in \IN$ and $m \le n$ is finitely presentable. All such objects form a small set. Moreover, any object of $\Mono$ is a filtered colimit of the subobjects $(F, F \cap X')$ where $F$ is a finite subset of $X$, and each $(F, F \cap X')$ is isomorphic to some $([n], [m])$. + - property: coregular proof: >- - For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. It suffices to show regular monomorphisms are stable under pushouts. Thus, suppose we have two morphisms $f : (X, X') \to (Y, Y')$ and $g : (X, X') \to (Z, Z')$ where $f$ is a regular monomorphism, which means $f$ is injective and $X' = f^{-1}(Y')$. Then we can construct a pushout diagram + It suffices to show regular monomorphisms are stable under pushouts. Thus, suppose we have two morphisms $f : (X, X') \to (Y, Y')$ and $g : (X, X') \to (Z, Z')$ where $f$ is a regular monomorphism, which means $f$ is injective and $X' = f^{-1}(Y')$. Then we can construct a pushout diagram $$\begin{CD} (X, X') @> f >> (Y, Y') \\ @V g VV @VV i_1 VV \\ @@ -83,102 +86,73 @@ satisfied_properties: \end{CD}$$ Here $i_1$ sends $f(x) \mapsto g(x) \in Z$ for $x \in X$, and otherwise it sends $y \mapsto y$ for $y \in Y \setminus f(X)$; and $i_2$ is the inclusion of $Z$. We certainly have $i_2$ is injective; it remains to show $i_2^{-1}(i_1(Y') \cup i_2(Z')) = Z'$. However, we have $$i_2^{-1}(i_1(Y') \cup i_2(Z')) = i_2^{-1}(i_1(Y')) \cup i_2^{-1}(i_2(Z'))$$ - and obviously $i_2^{-1}(i_2(Z')) = Z'$. Therefore, it suffices to show $i_2^{-1}(i_1(Y')) \subseteq Z'$. Thus, suppose we have $z \in Z$ such that $i_2(z) \in i_1(Y')$. That means there exists $y' \in Y'$ such that $z = i_1(y')$. But in order for $i_1(y')$ to land in the $Z$ portion of $(Y \setminus f(X)) \sqcup Z$, we must have $i_1(y') \in f(X)$. That means there exists $x \in X$ such that $f(x) = y'$; and by the assumption on $f$, in fact $x \in X'$. Therefore, $i_2(g(x)) = i_1(f(x)) = y' = i_2(z)$, so $z = g(x) \in Z'$. + and obviously $i_2^{-1}(i_2(Z')) = Z'$. Therefore, it suffices to show $i_2^{-1}(i_1(Y')) \subseteq Z'$. Thus, suppose we have $z \in Z$ such that $i_2(z) \in i_1(Y')$. That means there exists $y' \in Y'$ such that $z = i_1(y')$. But in order for $i_1(y')$ to land in the $Z$ portion of $(Y \setminus f(X)) \sqcup Z$, we must have $y' \in f(X)$. That means there exists $x \in X$ such that $f(x) = y'$; and by the assumption on $f$, in fact $x \in X'$. Therefore, $i_2(g(x)) = i_1(f(x)) = i_1(y') = z = i_2(z)$, so $z = g(x) \in Z'$. - property: co-Malcev proof: >- - For this proof we will work in the equivalent category of pairs $(X, X')$ where $X' \subseteq X$. Thus, suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is surjective. Since $\Set$ is co-Malcev, it follows that $E \simeq X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $r(i_1(x)) = x \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. + Suppose we have a coreflexive corelation $p : (X \sqcup X, X' \sqcup X') \twoheadrightarrow (E, E')$ with coreflexivity morphism $r : (E, E') \to (X, X')$. From the assumption that $p$ is an epimorphism, we have that $p : X \sqcup X \to E$ is a surjective function. Since $\Set$ is co-Malcev, it follows that $E \cong X \sqcup_Y X$ for some subset $Y \subseteq X$. It remains to show that $E' = i_1(X') \cup i_2(X') \subseteq X \sqcup_Y X$. Certainly, since we have a morphism $(X \sqcup_Y X, i_1(X') \cup i_2(X')) \to (E, E')$ induced by $p$, we must have $i_1(X') \cup i_2(X') \subseteq E'$. On the other hand, any element of $E'$ is an element of $E$ and hence is equal to either $i_1(x)$ or $i_2(x)$ for $x \in X$. In the first case, we must have $x = r(i_1(x)) \in X'$, so $i_1(x) \in i_1(X')$; and similarly for the second case. - property: effective cocongruences - proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \to X \sqcup_Y X$.' + proof: 'See the proof that $\Mono$ is co-Malcev: It shows that in fact any coreflexive corelation is equivalent to an effective cocongruence $X \sqcup X \twoheadrightarrow X \sqcup_Y X$.' unsatisfied_properties: - property: skeletal - proof: Consider the objects $X \xhookrightarrow{\id} X$ and $Y \xhookrightarrow{\id} Y$ for isomorphic but non-equal sets $X$ and $Y$. + proof: Consider the objects $(X, X)$ and $(Y, Y)$ for isomorphic but non-equal sets $X$ and $Y$. - property: balanced - proof: The unique morphism from $0 \hookrightarrow 1$ to $1 \hookrightarrow 1$ is both a monomorphism and an epimorphism, but not an isomorphism (see descriptions below). + proof: The unique morphism from $(1, 0)$ to $(1, 1)$ is both a monomorphism and an epimorphism, but not an isomorphism (see descriptions below). - property: cofiltered-limit-stable epimorphisms proof: >- - Consider the sequence of epimorphisms - $$\begin{CD} - \IN_{\ge n} @> \id >> \IN_{\ge n} \\ - @V ! VV @VV ! V \\ - 1 @>> \id > 1. - \end{CD}$$ - The limit is - $$\begin{CD} - 0 @> \id >> 0 \\ - @V ! VV @VV ! V \\ - 1 @>> \id > 1 - \end{CD}$$ - which is not an epimorphism. + We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here to the functor $\Set \to \Mono$ which sends a set $X$ to the pair $(X, X)$. - property: Malcev - proof: This is clear since $\Set$ is not Malcev, and it has a left exact embedding in $\Mono$ via the functor sending a set $X$ to $X \xhookrightarrow{\id} X$. + proof: This is clear since $\Set$ is not Malcev, and it has a left exact embedding in $\Mono$ via the functor sending a set $X$ to $(X, X)$. special_objects: initial object: - description: the unique function $0 \to 0$ + description: $(0, 0)$ terminal object: - description: the unique function $1 \to 1$ + description: $(1, 1)$ coproducts: - description: component-wise defined disjoint union, equipped with the disjoint union of the functions + description: component-wise defined disjoint union products: - description: component-wise defined cartesian product, equipped with the product function + description: component-wise defined cartesian product special_morphisms: isomorphisms: - description: pairs $(\ell, r)$ where $\ell$ and $r$ are both bijections + description: >- + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a bijection between $X$ and $Y$, and $f(X') = Y'$ proof: This is easy. monomorphisms: - description: pairs $(\ell, r)$ where $r$ is an injective function, from which it automatically follows that $\ell$ is also injective - proof: For the non-trivial direction, use the fact that the codomain functor taking an object $(X, Y, f)$ to $Y$ and a morphism $(\ell, r)$ to $r$ is representable by $0 \hookrightarrow 1$. + description: >- + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$ + proof: >- + For the non-trivial direction, use the fact that the functor taking an object $(X, X')$ to $X$ and a morphism $f : (X, X') \to (Y, Y')$ to the function $f : X \to Y$ is representable by $(1, 0)$. epimorphisms: - description: pairs $(\ell, r)$ where $r$ is a surjective function + description: >- + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$ proof: >- - Suppose we have a morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ such that $r$ is surjective. To see it is an epimorphism, suppose we have two morphisms $(\ell_1, r_1), (\ell_2, r_2) : (X', Y', g) \rightrightarrows (T, U, h)$ such that $(\ell_1, r_1) \circ (\ell, r) = (\ell_2, r_2) \circ (\ell, r)$. Then $r_1 \circ r = r_2 \circ r$ implies $r_1 = r_2$. It automatically follows that $\ell_1 = \ell_2$ since $h$ is a monomorphism in $\Set$. - - Conversely, suppose we have an epimorphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$. Then for any set $T$, the morphisms $(X', Y', g) \to (T, T, \id_T)$ are equivalent to the functions $Y' \to T$; therefore, $r$ is an epimorphism in $\Set$. + For the non-trivial direction, use the fact that the forgetful functor $\Mono \to \Set$, $(X, X') \mapsto X$, has a right adjoint given by $X \mapsto (X, X)$. Therefore, the forgetful functor preserves epimorphisms; so if $f : (X, X') \to (Y, Y')$ is an epimorphism in $\Mono$, then $f : X \to Y$ is an epimorphism in $\Set$ and therefore surjective. regular monomorphisms: description: >- - pairs $(\ell, r)$ where $r$ is an injective function and moreover the commutative square - $$\begin{CD} - X @> f >> Y \\ - @V \ell VV @VV r V \\ - X' @>> g > Y' - \end{CD}$$ - is in fact a cartesian square + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is an injective function from $X$ to $Y$, and $f^{-1}(Y') = X'$ (in particular, if $f : X \to Y$ is an inclusion map, then this is equivalent to $X' = X \cap Y'$) proof: >- To show any regular monomorphism satisfies this condition, suppose we have an equalizer diagram $$\begin{CD} - X @> f >> Y \\ - @V \ell VV @VV r V \\ - X' @> g >> Y' \\ - @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\ - X'' @>> h > Y''. + (X, X') @> f >> (Y, Y') @> g > h > (Z, Z'). \end{CD}$$ - Without loss of generality, we may assume $f$, $g$, $h$, $\ell$, and $r$ are all inclusion maps. Now suppose we have $y' \in Y'$ which is in the intersection of $X'$ and $Y$. Then $y' \in Y$ implies $r_1(y') = r_2(y')$. Therefore, since $h$ is injective, we can conclude $\ell_1(y') = \ell_2(y')$, so in fact $y' \in X$. This shows $X' \cap Y \subseteq X$; the other inclusion is automatic from the commutativity of the diagram. + We need to show $f^{-1}(Y') = X'$. From the definitions, we automatically get $X' \subseteq f^{-1}(Y')$. For the other inclusion, suppose we have $x \in X$ such that $f(x) \in Y'$. Then certainly $g(f(x)) = h(f(x)) \in Z'$, so $x'$ is in the equalizer of $g |_{Y'}, h |_{Y'} : Y' \rightrightarrows Z'$, which by definition is exactly $X'$. - To show any morphism satisfying this condition is a regular monomorphism, we may again assume $f$, $g$, $\ell$, and $r$ are all inclusion maps. We can then construct an equalizer diagram + For the other direction, suppose we are given a morphism $f : (X, X') \to (Y, Y')$ satisfying this condition. We can then construct an equalizer diagram $$\begin{CD} - X @> f >> Y \\ - @V \ell VV @VV r V \\ - X' @> g >> Y' \\ - @V \chi_X V \top_{X'} V @V \chi_Y V \top_{Y'} V \\ - \{ \top, \bot \} @> \id >> \{ \top, \bot \}. + (X, X') @> f >> (Y, Y') @> \chi_{f(X)} > \top_Y > (\{ \top, \bot \}, \{ \top, \bot \}). \end{CD}$$ - Here $\top_{X'}$ represents the constant function on $X'$ with value $\top$, and similarly for $\top_{Y'}$. Here, the assumption $X = X' \cap Y$ is used to establish the commutativity of the characteristic morphism $(\chi_X, \chi_Y) : (X', Y', g) \to (\{ \top, \bot \}, \{ \top, \bot \}, \id)$. + Here $\chi_{f(X)} : Y \to \{ \top, \bot \}$ is the characteristic function of the subset $f(X) \subseteq Y$, and $\top_Y$ is the constant function on $Y$ with value $\top$. regular epimorphisms: - description: pairs $(\ell, r)$ where both $\ell$ and $r$ are surjective functions + description: >- + morphisms $f : (X, X') \to (Y, Y')$ such that $f$ is a surjective function from $X$ to $Y$, and $f(X') = Y'$ proof: >- - To show any regular epimorphism satisfies this condition, suppose we have a parallel pair - $$\begin{CD} - X @> f >> Y \\ - @V \ell_1 V \ell_2 V @V r_1 V r_2 V \\ - X' @> g >> Y'. - \end{CD}$$ - To form the coequalizer in $\Mono$, first we may form the coequalizer in $\Set^{\rightarrow}$, $\coeq(\ell_1, \ell_2) \xrightarrow{\bar g} \coeq(r_1, r_2)$. Note this is not injective in general; however, we may apply the reflector to get the coequalizer $\im(\bar g) \hookrightarrow \coeq(r_1, r_2)$ in $\Mono$. Here, clearly the map $Y' \to \coeq(r_1, r_2)$ is surjective. Likewise, both the functions $X' \to \coeq(\ell_1, \ell_2)$ and $coeq(\ell_1, \ell_2) \to \im(\bar g)$ are surjective, so their composition $X' \to \coeq(\ell_1, \ell_2)$ is surjective as well. + To show any regular epimorphism satisfies this condition, suppose we have a parallel pair $g, h : (Z, Z') \rightrightarrows (X, X')$. To form the coequalizer in $\Mono$, first we form the coequalizer $f : X \to Y$ in $\Set$ of the underlying functions $g$ and $h$. Then by the construction of colimits in the proof of cocompleteness above, the coequalizer in $\Mono$ is $(Y, f(X') \cup f(g(Z')) \cup f(h(Z')))$. However, certainly $f(g(Z')) \subseteq f(X')$ and $f(h(Z')) \subseteq f(X')$, so this coequalizer reduces to $(Y, f(X'))$ and we see $f(X') = Y'$. - To show any morphism $(\ell, r) : (X, Y, f) \to (X', Y', g)$ satisfying this condition is a regular epimorphism, note that the kernel pair of $(\ell, r)$ can be computed component-wise. Therefore, the coequalizer in $\Set^{\rightarrow}$ of this kernel pair is exactly $(X', Y', g)$, so applying the reflector does nothing and $(X', Y', g)$ is also the coequalizer in $\Mono$. + To show any morphism $f : (X, X') \to (Y, Y')$ satisfying this condition is a regular epimorphism, note that the kernel pair of $f$ can be computed component-wise. Therefore, in general the coequalizer of the kernel pair of $f$ is $(f(X), f(X'))$; and with the given assumptions on $f$, this is isomorphic to $(Y, Y')$.